wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

updated examples in README to latest syntax

Browse source
This commit is contained in:
William Ball 2024-12-05 19:49:34 -08:00
parent 72e695a381
commit a3d72583b4
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
README.org
View file

@ -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.