From 72feeec46c34c678640341e76958481f4244d8df Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Thu, 12 Jan 2023 17:57:06 +0000 Subject: Provide examples of Obs code. This folder spells out the action of equality and cast for the different type constructors. Ideally the two correctness proofs should given by reflexivity. --- examples/equality/template.obs | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 examples/equality/template.obs (limited to 'examples/equality/template.obs') 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 -- cgit v1.2.3