diff options
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 |