summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2022-04-05Add another tiny proof.Greg Brown
2022-04-05Add a useful transport proof.Greg Brown
2022-04-05Add commutativity of reciprocal and power.Greg Brown
2022-04-05Add properties of multiplying to 0.Greg Brown
2022-04-05Generalise 0 comparison to ≤.Greg Brown
2022-04-05Minor clean up.Greg Brown
2022-04-04Add some more ordered division ring properties.Greg Brown
2022-04-04Add group inverse preserves identity.Greg Brown
2022-04-04Generalise the precondition for 0 < 1 in rings.Greg Brown
2022-04-04Remove redundant cancel property.Greg Brown
2022-04-02Add some properties of ordered fields.Greg Brown
2022-04-02Add properties of almost groups.Greg Brown
2022-04-02Add more properties for ordered structures.Greg Brown
2022-03-21Add all-in-one import for Hoare logic semantics.Greg Brown
2022-03-21Add some properties of algebraic pseudocode types.Greg Brown
2022-03-21Add missing renamings.Greg Brown
2022-03-20Rename Pseudocode.Types to something more sensibleGreg Brown
2022-03-20Fix incorrect defining properties of floor.Greg Brown
2022-03-19Add definition of Hoare logic semantics.Greg Brown
2022-03-19Modify pseudocode definition.Greg Brown
2022-02-15Make expressions unable to change state.Greg Brown
2022-02-15Remove unnecessary return-type part of StatementGreg Brown
2022-02-13Add Barrett implementation to EverythingGreg Brown
2022-02-13Write pseudocode definition of Barrett reductionGreg Brown
2022-02-13Define vmla instruction.Greg Brown
2022-02-13Extract common code from pseudocode instructionsGreg Brown
2022-02-13Refactor to group instruction definitions togetherGreg Brown
2022-02-13Finish definition of denotational semantics.Greg Brown
2022-02-02Add Helium.Data.Pseudocode to Everything.Greg Brown
2022-02-02Define pseudocode for a number of instructions.Greg Brown
2022-01-21Add pseudocode as a data type.Greg Brown
2022-01-19Rename pseudocode file.Greg Brown
2022-01-18Define the semantics of pseudocode data types.Greg Brown
2022-01-16Define ordered algebraic structures.Greg Brown
2022-01-12Eliminate even more state from the denotational semantics.Greg Brown
2022-01-08Make RawPseudocode contain its own bundles.Greg Brown
2022-01-08Update Everything.Greg Brown
2022-01-07Add a missing raw algebra.Greg Brown
2022-01-07Demonstrate pointwise Vectors inherit algebraic properties.Greg Brown
2022-01-07Add some required algebraic types.Greg Brown
2022-01-07Introduce semantics for sequences of instructions.Greg Brown
2022-01-07Introduce various housekeeping changesGreg Brown
2022-01-07Rename ⟦_⟧ to float.Greg Brown
2021-12-28Make the denotational semantics total.Greg Brown
2021-12-27Introduce Everything.agda to aid in overall compilation.Greg Brown
2021-12-21Define execBeats, a wrapper to execute beat-wise instructions.Greg Brown
2021-12-21Define semantics of vqdmulh.Greg Brown
2021-12-21Define semantics for vmulh.Greg Brown
2021-12-20Define vsub.Greg Brown
2021-12-20Remove bitstring addition.Greg Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 13:13:16 +0000