diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-12 17:57:06 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-12 17:57:06 +0000 |
| commit | 72feeec46c34c678640341e76958481f4244d8df (patch) | |
| tree | 3480dc151716912ffd2bba6d21bcc69798f844b9 /examples/equality/template.obs | |
| parent | bfba6b295a8cdf7321d939f22fbdd04d45408e63 (diff) | |
This folder spells out the action of equality and cast for the different
type constructors. Ideally the two correctness proofs should given by
reflexivity.
Diffstat (limited to 'examples/equality/template.obs')
| -rw-r--r-- | examples/equality/template.obs | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/examples/equality/template.obs b/examples/equality/template.obs new file mode 100644 index 0000000..856e05f --- /dev/null +++ b/examples/equality/template.obs @@ -0,0 +1,22 @@ +postulate TypeData : Set 1 +postulate Value : (type : TypeData) -> Set +postulate Equality : (left : TypeData) -> (right : TypeData) -> Prop +postulate Cast : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Value newType + +postulate EqualityCorrect : + (left : TypeData) -> + (right : TypeData) -> + Equality left right ~ (Value left ~ Value right) + +postulate CastCorrect : + (oldType : TypeData) -> + (newType : TypeData) -> + (equality : Equality oldType newType) -> + (value : Value oldType) -> + Cast oldType newType equality value ~ + cast (Value oldType) (Value newType) (fst (EqualityCorrect oldType newType) equality) value |