From dede63ab616d9111357776b3dca9f1e148945cb7 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Fri, 4 Dec 2015 14:19:41 -0500 Subject: [PATCH] minor changes --- examples/shortsetquot.ctt | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/examples/shortsetquot.ctt b/examples/shortsetquot.ctt index 18517b7..c76aa39 100644 --- a/examples/shortsetquot.ctt +++ b/examples/shortsetquot.ctt @@ -185,6 +185,12 @@ test' : (P' true').1 = K' true' test'' : Id (P' true').1 test test' = (P' true').2 test test' +-- These two terms are not convertible: +-- test' : Id (P' true').1 (K' true') +-- (hdisj_in1 (Id (setquot bool R.1) true' true') (Id (setquot bool R.1) true' false') (<_> true')) = +-- <_> K' true' + + -- Another test: @@ -230,6 +236,7 @@ bar (x : bool') : or (Id bool' x true') (Id bool' x false') -> inl p -> inl (hinhpr (Id bool' x true') p) inr p -> inr (hinhpr (Id bool' x false') p) +-- finally the map: foo (x : bool') : bool = f x rem where rem : or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 = @@ -237,7 +244,9 @@ foo (x : bool') : bool = f x rem (or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1,test3 x) (bar x) (K' x) --- This should evaluate to true?? +-- > :n testfoo +-- NORMEVAL: true +-- Time: 0m0.490s testfoo : bool = foo true' @@ -249,12 +258,7 @@ testfoo : bool = foo true' ntrue' : bool' = (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])) --- Why is this not working? +-- Why is this not working? Bug in pretty printer? -- ntest : (P' true').1 = \(P : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : or (IdP ( sig (bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) (\(A : bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) -> sig (sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP ( bool) x1 x2))))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))), IdP ( sig (bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) (\(A : bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) -> sig (sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP ( bool) x1 x2))))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))) ((\(x : bool) -> (IdP ( bool) false x,lem7 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) false x)) -> P0.1) -> f ((false, false)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) false x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> false, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) false x1) -> \(X2 : IdP ( bool) false x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])))) -> P.1) -> f (inl ( (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f0 : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f0 ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])))) - --- This is not true: --- test' : Id (P' true').1 (K' true') --- (hdisj_in1 (Id (setquot bool R.1) true' true') (Id (setquot bool R.1) true' false') (<_> true')) = --- <_> K' true' -- 2.34.1