From 87bac07cee90de290e9f3060d6e57939cbb363aa Mon Sep 17 00:00:00 2001 From: Anders Date: Wed, 15 Apr 2015 11:47:38 +0200 Subject: [PATCH] Finish example of integers as a HIT --- examples/integer.ctt | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) diff --git a/examples/integer.ctt b/examples/integer.ctt index 58e8d99..308525a 100644 --- a/examples/integer.ctt +++ b/examples/integer.ctt @@ -40,26 +40,13 @@ toZK : (a : Z) -> Id Z (toZ (fromZ a)) a = split inl n -> refl Z (inl n) inr n -> refl Z (inr n) --- fromZ (toZ (neg zero)) = fromZ (fun zero) --- = fromZ zeroZ --- = fromZ (inr zero) --- = pos zero - --- fromZ (toZ (neg (suc n)) = fromZ (fun (suc n)) --- = fromZ (inl n) --- = neg (suc n) - -sq : Square int (pos zero) (pos zero) (refl int (pos zero)) - (pos zero) (neg zero) zeroP' - (refl int (pos zero)) zeroP' = undefined - fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split pos n -> refl int (pos n) neg n -> rem n where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split zero -> zeroP' suc n -> refl int (neg (suc n)) - zeroP @ i -> sq @ i + zeroP @ i -> zeroP' @ i /\ j isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK -- 2.34.1