b678d7c · Idris-dev · git.iko.soy

CHANGELOG+4

compare with master

unifiedsplit

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

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

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

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

12

16

13Library updates

17Library updates

14---------------

18---------------

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

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

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

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

19

20−

21−

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

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

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

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

24 map g x = pure g <*> x

22 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

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

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

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

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

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

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

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

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

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

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

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

32

30

33−

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

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

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

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

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

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

37 mx >>= \x =>

34 mx >>= \x =>

38 pure (f x)

35 pure (f x)

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

36 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

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

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

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

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

43

40

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

53

50

54

51

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

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

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

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

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

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

58

55

59-- instance VerifiedMonoid Nat where

56-- instance VerifiedMonoid Nat where

60-- monoidNeutralIsNeutralL = plusZeroRightNeutral

57-- monoidNeutralIsNeutralL = plusZeroRightNeutral

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

65 monoidNeutralIsNeutralR xs = Refl

62 monoidNeutralIsNeutralR xs = Refl

66

63

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

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

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

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

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

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

70

67

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

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

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

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

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

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

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

78

75

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

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

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

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

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

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

82

79

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

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

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

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

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

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

86

83

87

84

88class JoinSemilattice a => VerifiedJoinSemilattice a where

85class JoinSemilattice a => VerifiedJoinSemilattice a where

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

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

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

97

94

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

95class (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

100

97

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

98class (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

103

100

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

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

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

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

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

110

107

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

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

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

109-- 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

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

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

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

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

116

113

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

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

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

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

115class RingWithUnity a => Field a where

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

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

117

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

119sum' = concat

libs/effects/Effects.idr+3−3

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

325|||

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

327%no_implicit

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

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

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

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

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

331

332||| 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)

346||| @env The environment to use.

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

348%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

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

351

352%no_implicit

src/Idris/AbsSyntaxTree.hs+57−24

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

2247

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

2249implicitNamesIn :: [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

2251 where

2253 where

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+

2252− ni 0 env (PRef _ _ n)

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

2253 | not (n `elem` env)

2273 | not (n `elem` env)

2254− = case lookupTy n (tt_ctxt ist) of

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

2255− [] -> [n]

2275+ = addFn n

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

2276+ ni 0 env (PRef _ _ n)

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

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

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

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

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

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

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

2260− ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (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)

2261− ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (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)

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

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

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

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

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

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

2292+ (imps, fns) <- get

2293+ put ([] ,[])

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

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

2295+ (impsfst, _) <- get

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

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

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

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

2298+ ni 0 env (PLam fc n _ ty sc) = do 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

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

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

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

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

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

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

2302+ ni 0 env (PPair _ _ _ l r) = do 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

2303+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do 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

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

2305+ ni 0 env t

2306+ ni 0 env r

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

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

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

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

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

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

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

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

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

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

2279

2312

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

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

2281− maybe [] (ni i env) ty

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

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

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

2283

2316

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

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

2285

2318

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

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

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

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

src/Idris/Elab/Term.hs−1

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

611 [] -> False

612 _ -> True

613 bindable (NS _ _) = False

614− bindable (UN xs) = True

615 bindable n = implicitable n

614 bindable n = implicitable n

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

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

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

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

test/basic009/expected+11−2

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

1MAIN-PASS

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

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

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

3+Type mismatch between

4+ 0 = 0 (Type of Refl)

5+and

6+ num = 0 (Expected type)

7+

8+Specifically:

9+ Type mismatch between

10+ 0

11+ and

12+ num

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

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

test/classes001/ClassName.idr+1−1

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

21test1 : twiceAString 2 = "22"

22test1 = Refl

23

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

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

25test2 = Refl

26

27

test/dsl003/DSLPi.idr+1−1

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

43test3 : Spec []

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

45

46−test4 : test2 = test3

46+test4 : DSLPi.test2 = DSLPi.test3

47test4 = Refl

test/error003/expected+1−1

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

1ErrorReflection.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"

13firstSentence : String

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

15

16−emptyTest : prim__strSubstr 100000 14 firstSentence = ""

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

17emptyTest = Refl

18

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

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

20multiTest = Refl

21

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

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

23negative = Refl

24

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

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

26negativeEnd = Refl

27

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

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

29negativeLength = Refl

30

31main : IO ()

test/proof003/test015.idr+1−1

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

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

107

108Main.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

110 rewrite sym (plusZeroRightNeutral x);

111 rewrite sym (plusZeroRightNeutral v1);

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

test/proofsearch001/proofsearch001.idr+1−1

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

1%default total

2

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

4−instance C Int not where {}

4+instance C Int Bool.not where {}

5

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

7foo = ()

test/quasiquote006/quasiquote006.idr+2−2

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

2a : TTName

3a = `{Nat}

4

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

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

6aOK = Refl

7

8b : TTName

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

17d : TTName

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

19

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

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

21dOK = Refl

test/reg001/reg001.idr+1−1

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

7import Control.Isomorphism

8

9class 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

11

12data Imp : Type where

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

test/reg041/ott.idr+1−1

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

37EQ (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)

38EQ _ _ _ _ = zero

39

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

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

41example = ?prf

42

test/reg047/reg047.idr+5−5

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

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

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

5

6−data Nat = zero | succ Nat

6+data Nat = Zero | Succ Nat

7

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

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

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

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

12IdRefl A a = Refl {x = a}

13

14−zzz : Id Nat zero zero

14+zzz : Id Nat Zero Zero

15−zzz = IdRefl Nat zero

15+zzz = IdRefl Nat Zero

16

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

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

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

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

test/reg047/reg047a.idr+7−7

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

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

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

5

6−data MNat = zero | succ MNat

6+data MNat = Zero | Succ MNat

7

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

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

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

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

12IdRefl A a = Refl {x = a}

13

14−zzzz : Id MNat zero zero

14+zzzz : Id MNat Zero Zero

15−zzzz = IdRefl MNat zero

15+zzzz = IdRefl MNat Zero

16

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

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

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

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

19

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

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

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

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

22

23

24