diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-18 15:05:24 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-18 15:21:38 +0100 |
| commit | 00a0ce9082b4cc1389815defcc806efd4a9b80f4 (patch) | |
| tree | aebdc99b954be177571697fc743ee75841c98b2e /src/Helium/Tactic/CommutativeRing/NonReflective.agda | |
| parent | 24845ef25e12864711552ebc75a1f54903bee50c (diff) | |
Do a big refactor.
- Replace the decidable predicates on expressions and statements with
separate data types.
- Reorganise the Hoare logic semantics to remove unnecessary
definitions.
- Make liberal use of modules to group related definitions together.
- Unify the types for denotational and Hoare logic semantics.
- Make bits an abstraction of array types.
Diffstat (limited to 'src/Helium/Tactic/CommutativeRing/NonReflective.agda')
0 files changed, 0 insertions, 0 deletions