From fd54a6d0e5bc702a7646e698a9d7d75c39f86dfc Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 21 Apr 2015 10:10:51 +0200 Subject: [PATCH] Fix examples --- examples/equiv.ctt | 2 +- examples/integer.ctt | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/examples/equiv.ctt b/examples/equiv.ctt index 4beebb5..ef097f2 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -63,6 +63,6 @@ lemEquivFib (A:U) (F G :A -> U) (f:(x:A) -> F x -> G x) where yu : AF = z.1 y : A = yu.1 w : F y = yu.2 - p : Id A x y = (rem3 @ i).1 + p : Id A x y = (z.2 @ i).1 q : IdP (G (p@j)) v (f y w) = ((z.2) @ i).2 rem7 (z0 z1 : fiber (F x) (G x) (f x) v) : Id (fiber (F x) (G x) (f x) v) z0 z1 = psi ((rem1.1 (phi z0) (phi z1))@i) diff --git a/examples/integer.ctt b/examples/integer.ctt index 57c5db2..6e3ed0c 100644 --- a/examples/integer.ctt +++ b/examples/integer.ctt @@ -26,9 +26,9 @@ predInt : int -> int = split toZ : int -> Z = split pos n -> inr n - neg n -> fun n - where fun : nat -> Z = split - zero -> zeroZ + neg n -> auxToZ n + where auxToZ : nat -> Z = split + zero -> inr zero suc n -> inl n zeroP @ i -> zeroZ -- 2.34.1