From a3d72583b446366c9d4417f42f1b4067c967a15f Mon Sep 17 00:00:00 2001 From: William Ball Date: Thu, 5 Dec 2024 19:49:34 -0800 Subject: [PATCH] updated examples in README to latest syntax --- README.org | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README.org b/README.org index 14d3f03..e5d5aee 100644 --- a/README.org +++ b/README.org @@ -119,20 +119,20 @@ Here is an example file defining Leibniz equality and proving that it is reflexi -- Defining Leibniz equality -- Note that we can leave the ascription off - eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y; + def eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y; -- Equality is reflexive, which is easy to prove -- Here we give an ascription so that when `perga` reports the type, -- it references `eq` rather than inferring the type. - eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx; + def eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx; -- Equality is symmetric. This one's a little harder to prove. - eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := + def eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) => Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy; -- Equality is transitive. - eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := + def eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) => Hyz P (Hxy P Hx); #+end_src Running =perga equality.pg= yields the following output.