summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2024-01-22Fix invalid statementHEADmasterGreg Brown
2023-07-25Prove mgu has a unique factor.Greg Brown
2023-07-25Remove SFin.Greg Brown
Delete unused modules. Restructure some proofs to reduce the number of lemmas.
2023-07-16Minor changes for use by other projects.Greg Brown
2023-07-12Add constructor for signature.Greg Brown
2023-07-12Prove unification correct.Greg Brown
2023-07-11Promote property equivalence to a record.Greg Brown
Improves inference for congruence.
2023-07-11Begin big unification proof.Greg Brown
2023-07-11Use new notion of Fin to reduce casts.Greg Brown
2023-07-10Describe unification.Greg Brown
2023-07-10Prove the optimist's lemma.Greg Brown
2023-07-07Add occurs check for terms.Greg Brown
2023-07-07Define properties of substitutions.Greg Brown
2023-06-30Define zippers and prove no cycles exist.Greg Brown
2023-06-30Define thinning and thickening.Greg Brown
2023-06-30Define terms, renaming and substitution.Greg Brown
2023-06-30Initial commit.Greg Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 22:46:34 +0000