index
:
yellowsquid/helium.git
abstract
axiomatic
dev/bitvec-arith
last-attempt
master
[no description]
Chloe Brown
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Helium
/
Algebra
/
Ordered
/
StrictTotal
Age
Commit message (
Collapse
)
Author
2022-04-09
Add some more algebraic properties.
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
It is in the standard library as `⁻¹-injective`.
2022-04-02
Add some properties of ordered fields.
Greg Brown
2022-04-02
Add more properties for ordered structures.
Greg Brown
2022-03-21
Add some properties of algebraic pseudocode types.
Greg Brown
2022-03-21
Add missing renamings.
Greg Brown
2022-01-18
Define the semantics of pseudocode data types.
Greg Brown
2022-01-16
Define ordered algebraic structures.
Greg Brown
