b678d7c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Changed scoping rules for unbound implicits.

Any name which would be a valid unbound implicit is now *always* an unbound implicit. This is much more resilient to changes in inputs, but does require that function names be explicitly qualified when in argument position. Updated libraries/tests accordingly. WARNING: This is likely to break some code; the fix is, in all cases, to give explicit namespaces for function names in types in an argument position (i.e. a valid position for it to be an unbound implicit).

commitb678d7c93cf577e28be2d1cea4a17a223e6b0a28 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 21 Sep 2015, 17:21 (11 years ago) parentee76b88

18 files changed+115−73

compare with master

unifiedsplit

CHANGELOG+4 libs/contrib/Classes/Verified.idr+13−16 libs/contrib/Control/Algebra.idr+1−1 libs/effects/Effects.idr+3−3 src/Idris/AbsSyntaxTree.hs+57−24 src/Idris/Elab/Term.hs−1 test/basic009/expected+11−2 test/classes001/ClassName.idr+1−1 test/dsl003/DSLPi.idr+1−1 test/error003/expected+1−1 test/primitives001/substring.idr+5−5 test/proof003/test015.idr+1−1 test/proofsearch001/proofsearch001.idr+1−1 test/quasiquote006/quasiquote006.idr+2−2 test/reg001/reg001.idr+1−1 test/reg041/ott.idr+1−1 test/reg047/reg047.idr+5−5 test/reg047/reg047a.idr+7−7

CHANGELOG+4

@@ -9,6 +9,10 @@ Language updates

99 for defining new names. `{n} still quotes n to an existing name in scope.

1010* A new primitive operator prim__strSubstr for more efficient extraction of

1111 substrings. External code generators should implement this.

12+* Changed scoping rules for unbound implicits: any name which would be a

13+ valid unbound implicit is now *always* an unbound implicit. This is much

14+ more resilient to changes in inputs, but does require that function names

15+ be explicitly qualified when in argument position.

1216

1317Library updates

1418---------------

libs/contrib/Classes/Verified.idr+13−16

@@ -17,12 +17,10 @@ class Functor f => VerifiedFunctor (f : Type -> Type) where

1717 (g1 : a -> b) -> (g2 : b -> c) ->

1818 map (g2 . g1) x = (map g2 . map g1) x

1919

20−

21−

2220class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

2321 applicativeMap : (x : f a) -> (g : a -> b) ->

2422 map g x = pure g <*> x

25− applicativeIdentity : (x : f a) -> pure id <*> x = x

23+ applicativeIdentity : (x : f a) -> pure Basics.id <*> x = x

2624 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->

2725 ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)

2826 applicativeHomomorphism : (x : a) -> (g : a -> b) ->

@@ -30,14 +28,13 @@ class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Typ

3028 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

3129 g <*> pure x = pure (\g' : a -> b => g' x) <*> g

3230

33−

3431class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

3532 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->

3633 mf <*> mx = mf >>= \f =>

3734 mx >>= \x =>

3835 pure (f x)

3936 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x

40− monadRightIdentity : (mx : m a) -> mx >>= return = mx

37+ monadRightIdentity : (mx : m a) -> mx >>= Monad.return = mx

4138 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->

4239 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

4340

@@ -53,8 +50,8 @@ instance VerifiedSemigroup (List a) where

5350

5451

5552class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

56− total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l

57− total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r

53+ total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l

54+ total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r

5855

5956-- instance VerifiedMonoid Nat where

6057-- monoidNeutralIsNeutralL = plusZeroRightNeutral

@@ -65,8 +62,8 @@ instance VerifiedMonoid (List a) where

6562 monoidNeutralIsNeutralR xs = Refl

6663

6764class (VerifiedMonoid a, Group a) => VerifiedGroup a where

68− total groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral

69− total groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral

65+ total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral

66+ total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral

7067

7168class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

7269 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

@@ -77,12 +74,12 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

7774 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

7875

7976class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

80− total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l

81− total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r

77+ total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l

78+ total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r

8279

8380--class (VerifiedRingWithUnity a, Field a) => VerifiedField a where

84−-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity

85−-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity

81+-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = Algebra.unity

82+-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = Algebra.unity

8683

8784

8885class JoinSemilattice a => VerifiedJoinSemilattice a where

@@ -96,10 +93,10 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where

9693 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

9794

9895class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

99− total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = e

96+ total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e Algebra.bottom = e

10097

10198class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

102− total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = e

99+ total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e Algebra.top = e

103100

104101class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

105102 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

@@ -110,7 +107,7 @@ class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, Verif

110107

111108--class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

112109-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

113−-- total moduleScalarUnityIsUnity : (v : b) -> unity {a} <#> v = v

110+-- total moduleScalarUnityIsUnity : (v : b) -> Algebra.unity {a} <#> v = v

114111-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

115112-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

116113

libs/contrib/Control/Algebra.idr+1−1

@@ -113,7 +113,7 @@ class Ring a => RingWithUnity a where

113113||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

114114||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

115115class RingWithUnity a => Field a where

116− inverseM : (x : a) -> Not (x = neutral) -> a

116+ inverseM : (x : a) -> Not (x = Algebra.neutral) -> a

117117

118118sum' : (Foldable t, Monoid a) => t a -> a

119119sum' = concat

libs/effects/Effects.idr+3−3

@@ -325,8 +325,8 @@ run prog {env} = eff env prog (\r, env => pure r)

325325|||

326326||| @prog The effectful program to run.

327327%no_implicit

328−runPure : (prog : EffM id a xs xs') ->

329− {default MkDefaultEnv env : Env id xs} -> a

328+runPure : (prog : EffM Basics.id a xs xs') ->

329+ {default MkDefaultEnv env : Env Basics.id xs} -> a

330330runPure prog {env} = eff env prog (\r, env => r)

331331

332332||| Run an effectful program in a given context `m` with a default value for the environment.

@@ -346,7 +346,7 @@ runInit env prog = eff env prog (\r, env => pure r)

346346||| @env The environment to use.

347347||| @prog The effectful program to run.

348348%no_implicit

349−runPureInit : (env : Env id xs) -> (prog : EffM id a xs xs') -> a

349+runPureInit : (env : Env Basics.id xs) -> (prog : EffM Basics.id a xs xs') -> a

350350runPureInit env prog = eff env prog (\r, env => r)

351351

352352%no_implicit

src/Idris/AbsSyntaxTree.hs+57−24

@@ -2247,41 +2247,74 @@ boundNamesIn tm = S.toList (ni 0 S.empty tm)

22472247

22482248-- Return names which are valid implicits in the given term (type).

22492249implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

2250−implicitNamesIn uvars ist tm = nub $ ni 0 [] tm

2250+implicitNamesIn uvars ist tm

2251+ = let (imps, fns) = execState (ni 0 [] tm) ([], []) in

2252+ nub imps \\ nub fns

22512253 where

2252− ni 0 env (PRef _ _ n)

2254+ addImp n = do (imps, fns) <- get

2255+ put (n : imps, fns)

2256+ addFn n = do (imps, fns) <- get

2257+ put (imps, n: fns)

2258+

2259+ notCAF [] = False

2260+ notCAF (PExp _ _ _ _ : _) = True

2261+ notCAF (_ : xs) = notCAF xs

2262+

2263+ notHidden (n, _) = case getAccessibility n of

2264+ Hidden -> False

2265+ _ -> True

2266+

2267+ getAccessibility n

2268+ = case lookupDefAccExact n False (tt_ctxt ist) of

2269+ Just (n,t) -> t

2270+ _ -> Public

2271+

2272+ ni 0 env (PRef _ _ n@(NS _ _))

22532273 | not (n `elem` env)

2254− = case lookupTy n (tt_ctxt ist) of

2255− [] -> [n]

2256− _ -> if n `elem` uvars then [n] else []

2274+ -- Never implicitly bind if there's a namespace

2275+ = addFn n

2276+ ni 0 env (PRef _ _ n)

2277+ | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n

22572278 ni 0 env (PApp _ f@(PRef _ _ n) as)

2258− | n `elem` uvars = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2259− | otherwise = concatMap (ni 0 env) (map getTm as)

2260− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2261− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2262− ni 0 env (PCase _ c os) = ni 0 env c ++

2279+ | n `elem` uvars = do ni 0 env f

2280+ mapM_ (ni 0 env) (map getTm as)

2281+ | otherwise = do case lookupTy n (tt_ctxt ist) of

2282+ [] -> return ()

2283+ _ -> addFn n

2284+ mapM_ (ni 0 env) (map getTm as)

2285+ ni 0 env (PApp _ f as) = do ni 0 env f

2286+ mapM_ (ni 0 env) (map getTm as)

2287+ ni 0 env (PAppBind _ f as) = do ni 0 env f

2288+ mapM_ (ni 0 env) (map getTm as)

2289+ ni 0 env (PCase _ c os) = do ni 0 env c

22632290 -- names in 'os', not counting the names bound in the cases

2264− (nub (concatMap (ni 0 env) (map snd os))

2265− \\ nub (concatMap (ni 0 env) (map fst os)))

2266− ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2267− ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2268− ni 0 env (PPi p n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2269− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2270− ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2271− ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2272− ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2273− ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2274− ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2291+ mapM_ (ni 0 env) (map snd os)

2292+ (imps, fns) <- get

2293+ put ([] ,[])

2294+ mapM_ (ni 0 env) (map fst os)

2295+ (impsfst, _) <- get

2296+ put (nub imps \\ nub impsfst, fns)

2297+ ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]

2298+ ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2299+ ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2300+ ni 0 env (PRewrite _ l r _) = do ni 0 env l; ni 0 env r

2301+ ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

2302+ ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r

2303+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r

2304+ ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l

2305+ ni 0 env t

2306+ ni 0 env r

2307+ ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as

22752308 ni 0 env (PHidden tm) = ni 0 env tm

22762309 ni 0 env (PUnifyLog tm) = ni 0 env tm

22772310 ni 0 env (PDisamb _ tm) = ni 0 env tm

22782311 ni 0 env (PNoImplicits tm) = ni 0 env tm

22792312

2280− ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++

2281− maybe [] (ni i env) ty

2313+ ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm

2314+ maybe (return ()) (ni i env) ty

22822315 ni i env (PUnquote tm) = ni (i - 1) env tm

22832316

2284− ni i env tm = concatMap (ni i env) (children tm)

2317+ ni i env tm = mapM_ (ni i env) (children tm)

22852318

22862319-- Return names which are free in the given term.

22872320namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

src/Idris/Elab/Term.hs−1

@@ -611,7 +611,6 @@ elab ist info emode opts fn tm

611611 [] -> False

612612 _ -> True

613613 bindable (NS _ _) = False

614− bindable (UN xs) = True

615614 bindable n = implicitable n

616615 elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

617616 elab' ina fc' tm@(PRef fc hls n)

test/basic009/expected+11−2

@@ -1,4 +1,13 @@

11MAIN-PASS

2−Faulty.idr:6:7:When checking type of Faulty.fault:

3−Can't disambiguate name: A.num, B.C.num

2+Faulty.idr:7:7:When checking right hand side of fault:

3+Type mismatch between

4+ 0 = 0 (Type of Refl)

5+and

6+ num = 0 (Expected type)

8+Specifically:

9+ Type mismatch between

10+ 0

11+ and

12+ num

413Multiple.idr:3:1:import alias not unique: "X"

test/classes001/ClassName.idr+1−1

@@ -21,7 +21,7 @@ badShow = MkMyShow (const "hej")

2121test1 : twiceAString 2 = "22"

2222test1 = Refl

2323

24−test2 : twiceAString @{badShow} 2 = "hejhej"

24+test2 : twiceAString @{ClassName.badShow} 2 = "hejhej"

2525test2 = Refl

2626

2727

test/dsl003/DSLPi.idr+1−1

@@ -43,5 +43,5 @@ test2 = specs ((x, y : INT) -> x === y)

4343test3 : Spec []

4444test3 = ForAll INT . ForAll INT . ItHolds $ Var (FS FZ) === Var FZ

4545

46−test4 : test2 = test3

46+test4 : DSLPi.test2 = DSLPi.test3

4747test4 = Refl

test/error003/expected+1−1

@@ -1,2 +1,2 @@

11ErrorReflection.idr:68:5:When checking right hand side of bad:

2−DSL type error: (t(503) => t'(504)) doesn't match ()

2+DSL type error: (t(504) => t'(503)) doesn't match ()

test/primitives001/substring.idr+5−5

@@ -13,19 +13,19 @@ foo = "Hello! here's the thing"

1313firstSentence : String

1414firstSentence = "Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。"

1515

16−emptyTest : prim__strSubstr 100000 14 firstSentence = ""

16+emptyTest : prim__strSubstr 100000 14 Main.firstSentence = ""

1717emptyTest = Refl

1818

19−multiTest : prim__strSubstr 10 5 firstSentence = "用的依赖类"

19+multiTest : prim__strSubstr 10 5 Main.firstSentence = "用的依赖类"

2020multiTest = Refl

2121

22−negative : prim__strSubstr (-10) 5 firstSentence = "Idris"

22+negative : prim__strSubstr (-10) 5 Main.firstSentence = "Idris"

2323negative = Refl

2424

25−negativeEnd : prim__strSubstr 0 (-1) firstSentence = ""

25+negativeEnd : prim__strSubstr 0 (-1) Main.firstSentence = ""

2626negativeEnd = Refl

2727

28−negativeLength : prim__strSubstr 4 (-4) firstSentence = ""

28+negativeLength : prim__strSubstr 4 (-4) Main.firstSentence = ""

2929negativeLength = Refl

3030

3131main : IO ()

test/proof003/test015.idr+1−1

@@ -106,7 +106,7 @@ Main.ntbEven = proof {

106106-- There is almost certainly an easier proof. I don't care, for now :)

107107

108108Main.adc_lemma_2 = proof {

109− intro w,v,num0,v1,num1,x,bx,x1,bx1,bit0,b0,bit1,b1,c,bc

109+ intro v,w,num0,v1,num1,x,bx,x1,bx1,bit0,b0,bit1,b1,c,bc

110110 rewrite sym (plusZeroRightNeutral x);

111111 rewrite sym (plusZeroRightNeutral v1);

112112 rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));

test/proofsearch001/proofsearch001.idr+1−1

@@ -1,7 +1,7 @@

11%default total

33class C a (f : Bool -> Bool) | a where {}

4−instance C Int not where {}

4+instance C Int Bool.not where {}

66foo : C Int g => {auto pf : g True = False} -> Unit

77foo = ()

test/quasiquote006/quasiquote006.idr+2−2

@@ -2,7 +2,7 @@

22a : TTName

33a = `{Nat}

5−aOK : a = NS (UN "Nat") ["Nat", "Prelude"]

5+aOK : Main.a = NS (UN "Nat") ["Nat", "Prelude"]

66aOK = Refl

88b : TTName

@@ -17,5 +17,5 @@ d = `{(::)}

1717d : TTName

1818d = `{List.(::)}

1919

20−dOK : d = NS (UN "::") ["List", "Prelude"]

20+dOK : Main.d = NS (UN "::") ["List", "Prelude"]

2121dOK = Refl

test/reg001/reg001.idr+1−1

@@ -7,7 +7,7 @@ import Data.Fin

77import Control.Isomorphism

99class Functor f => VerifiedFunctor (f : Type -> Type) where

10− identity : (fa : f a) -> map id fa = fa

10+ identity : (fa : f a) -> map Basics.id fa = fa

1111

1212data Imp : Type where

1313 MkImp : {any : Type} -> any -> Imp

test/reg041/ott.idr+1−1

@@ -37,6 +37,6 @@ EQ two False two False = one

3737EQ (pi s t) f (pi s' t') g = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)

3838EQ _ _ _ _ = zero

3939

40−example : <| (id == id in (two ~> two)) |>

40+example : <| (Basics.id == Basics.id in (OTT.two ~> OTT.two)) |>

4141example = ?prf

4242

test/reg047/reg047.idr+5−5

@@ -3,7 +3,7 @@ module test

33data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

44 sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

6−data Nat = zero | succ Nat

6+data Nat = Zero | Succ Nat

88Id : (A : Type) -> A -> A -> Type

99Id A = (=) {A = A} {B = A}

@@ -11,8 +11,8 @@ Id A = (=) {A = A} {B = A}

1111IdRefl : (A : Type) -> (a : A) -> Id A a a

1212IdRefl A a = Refl {x = a}

1313

14−zzz : Id Nat zero zero

15−zzz = IdRefl Nat zero

14+zzz : Id Nat Zero Zero

15+zzz = IdRefl Nat Zero

1616

17−eep : TTSigma Nat (\ a => Id Nat a zero)

18−eep = sigma Nat (\ a => Id Nat a zero) zero zzz

17+eep : TTSigma Nat (\ a => Id Nat a Zero)

18+eep = sigma Nat (\ a => Id Nat a Zero) Zero zzz

test/reg047/reg047a.idr+7−7

@@ -3,7 +3,7 @@ module test

33data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

44 sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

6−data MNat = zero | succ MNat

6+data MNat = Zero | Succ MNat

88Id : (A : Type) -> A -> A -> Type

99Id = \A,x,y => x = y -- {a = A} {b = A}

@@ -11,14 +11,14 @@ Id = \A,x,y => x = y -- {a = A} {b = A}

1111IdRefl : (A : Type) -> (a : A) -> Id A a a

1212IdRefl A a = Refl {x = a}

1313

14−zzzz : Id MNat zero zero

15−zzzz = IdRefl MNat zero

14+zzzz : Id MNat Zero Zero

15+zzzz = IdRefl MNat Zero

1616

17−eep : TTSigma MNat (\ c => Id MNat c zero)

18−eep = (sigma MNat (\b => Id MNat b zero) zero zzzz)

17+eep : TTSigma MNat (\ c => Id MNat c Zero)

18+eep = (sigma MNat (\b => Id MNat b Zero) Zero zzzz)

1919

20−eep2 : TTSigma MNat (\ c => Id MNat c zero)

21−eep2 = (sigma MNat (\b => Id MNat b zero) zero (IdRefl MNat zero))

20+eep2 : TTSigma MNat (\ c => Id MNat c Zero)

21+eep2 = (sigma MNat (\b => Id MNat b Zero) Zero (IdRefl MNat Zero))

2222

2323

2424