yellowsquid/helium.git - [no description]

Age	Commit message (Expand)	Author
2022-04-09	Add some more algebraic properties.	Greg Brown
2022-04-07	Add a new ring solver tactic.	Greg Brown
2022-04-05	Add another tiny proof.	Greg Brown
2022-04-05	Add a useful transport proof.	Greg Brown
2022-04-05	Add commutativity of reciprocal and power.	Greg Brown
2022-04-05	Add properties of multiplying to 0.	Greg Brown
2022-04-05	Generalise 0 comparison to ≤.	Greg Brown
2022-04-05	Minor clean up.	Greg Brown
2022-04-04	Add some more ordered division ring properties.	Greg Brown
2022-04-04	Add group inverse preserves identity.	Greg Brown
2022-04-04	Generalise the precondition for 0 < 1 in rings.	Greg Brown
2022-04-04	Remove redundant cancel property.	Greg Brown
2022-04-02	Add some properties of ordered fields.	Greg Brown
2022-04-02	Add properties of almost groups.	Greg Brown
2022-04-02	Add more properties for ordered structures.	Greg Brown
2022-03-21	Add all-in-one import for Hoare logic semantics.	Greg Brown
2022-03-21	Add some properties of algebraic pseudocode types.	Greg Brown
2022-03-21	Add missing renamings.	Greg Brown
2022-03-20	Rename Pseudocode.Types to something more sensible	Greg Brown
2022-03-20	Fix incorrect defining properties of floor.	Greg Brown
2022-03-19	Add definition of Hoare logic semantics.	Greg Brown
2022-03-19	Modify pseudocode definition.	Greg Brown
2022-02-15	Make expressions unable to change state.	Greg Brown
2022-02-15	Remove unnecessary return-type part of Statement	Greg Brown
2022-02-13	Write pseudocode definition of Barrett reduction	Greg Brown
2022-02-13	Define vmla instruction.	Greg Brown
2022-02-13	Extract common code from pseudocode instructions	Greg Brown
2022-02-13	Refactor to group instruction definitions together	Greg Brown
2022-02-13	Finish definition of denotational semantics.	Greg Brown
2022-02-02	Define pseudocode for a number of instructions.	Greg Brown
2022-01-21	Add pseudocode as a data type.	Greg Brown
2022-01-19	Rename pseudocode file.	Greg Brown
2022-01-18	Define the semantics of pseudocode data types.	Greg Brown
2022-01-16	Define ordered algebraic structures.	Greg Brown
2022-01-12	Eliminate even more state from the denotational semantics.	Greg Brown
2022-01-08	Make RawPseudocode contain its own bundles.	Greg Brown
2022-01-07	Add a missing raw algebra.	Greg Brown
2022-01-07	Demonstrate pointwise Vectors inherit algebraic properties.	Greg Brown
2022-01-07	Add some required algebraic types.	Greg Brown
2022-01-07	Introduce semantics for sequences of instructions.	Greg Brown
2022-01-07	Rename ⟦_⟧ to float.	Greg Brown
2021-12-28	Make the denotational semantics total.	Greg Brown
2021-12-27	Introduce Everything.agda to aid in overall compilation.	Greg Brown
2021-12-21	Define execBeats, a wrapper to execute beat-wise instructions.	Greg Brown
2021-12-21	Define semantics of vqdmulh.	Greg Brown
2021-12-21	Define semantics for vmulh.	Greg Brown
2021-12-20	Define vsub.	Greg Brown
2021-12-20	Remove bitstring addition.	Greg Brown
2021-12-20	Extract structures shared by most binary vector operations.	Greg Brown
2021-12-20	Define vmul.	Greg Brown