mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 09:49:24 +03:00
Update tests
Well that was clever. I updated my tests locally and forgot to include them in the commit...
This commit is contained in:
Edwin Brady
parent
09c4b6cc03
commit
71b401d3de
@ -2,35 +2,13 @@ Dumping case trees to Main.cases
|
||||
prim__add_Integer = [{arg:N}, {arg:N}]: (+Integer [!{arg:N}, !{arg:N}])
|
||||
prim__sub_Integer = [{arg:N}, {arg:N}]: (-Integer [!{arg:N}, !{arg:N}])
|
||||
prim__mul_Integer = [{arg:N}, {arg:N}]: (*Integer [!{arg:N}, !{arg:N}])
|
||||
prim__lte_Integer = [{arg:N}, {arg:N}]: (<=Integer [!{arg:N}, !{arg:N}])
|
||||
prim__believe_me = [{arg:N}, {arg:N}, {arg:N}]: (believe_me [!{arg:N}, !{arg:N}, !{arg:N}])
|
||||
Main.plus = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 !{arg:N})] Just (%let {e:N} (-Integer [!{arg:N}, 1]) (+Integer [1, (Main.plus [!{e:N}, !{arg:N}])])))
|
||||
Main.main = [{ext:N}]: (Main.plus [(+Integer [1, 0]), (+Integer [1, (+Integer [1, 0])])])
|
||||
Main.Z = Constructor tag Just 1 arity 0
|
||||
Main.S = Constructor tag Just 0 arity 1
|
||||
Prelude.Basics.intToBool = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1)] Just 0)
|
||||
Prelude.Basics.True = Constructor tag Just 0 arity 0
|
||||
Prelude.Basics.False = Constructor tag Just 1 arity 0
|
||||
Builtin.believe_me = [{ext:N}]: (believe_me [___, ___, !{ext:N}])
|
||||
Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [!{arg:N}])), (%constcase 1 0)] Nothing)
|
||||
Prelude.Types.prim__integerToNat = [{arg:N}]: (Prelude.Types.case block in prim__integerToNat [!{arg:N}, (%case (<=Integer [0, !{arg:N}]) [(%constcase 0 1)] Just 0)])
|
||||
Prelude.Types.Z = Constructor tag Just 0 arity 0
|
||||
Prelude.Interfaces.Functor at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 2 (newtype by 1)
|
||||
Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Interfaces.pure = [{arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{ext:N}]))] Nothing)
|
||||
PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, !{arg:N}])
|
||||
PrimIO.case block in case block in io_bind = [{arg:N}, {arg:N}, {arg:N}]: (!{arg:N} [!{arg:N}])
|
||||
PrimIO.case block in io_bind = [{arg:N}, {arg:N}]: (PrimIO.case block in case block in io_bind [!{arg:N}, ___, (!{arg:N} [!{arg:N}])])
|
||||
PrimIO.unsafePerformIO = [{arg:N}]: (PrimIO.unsafeCreateWorld [(%lam w (PrimIO.case block in unsafePerformIO [!{arg:N}, (!{arg:N} [!w])]))])
|
||||
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}]: !{arg:N}
|
||||
PrimIO.unsafeCreateWorld = [{arg:N}]: (!{arg:N} [%MkWorld])
|
||||
PrimIO.io_pure = [{arg:N}, {ext:N}]: !{arg:N}
|
||||
PrimIO.io_bind = [{arg:N}, {arg:N}, {ext:N}]: (PrimIO.case block in io_bind [!{arg:N}, (!{arg:N} [!{ext:N}])])
|
||||
PrimIO.MkIORes = Constructor tag Just 0 arity 3 (newtype by 1)
|
||||
PrimIO.MkIO = Constructor tag Just 0 arity 2 (newtype by 1)
|
||||
Prelude.IO.pure = [{arg:N}, {ext:N}]: !{arg:N}
|
||||
Prelude.IO.map = [{arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (!{arg:N} [!{act:N}]))
|
||||
Prelude.IO.Functor implementation at Prelude/IO.idr:L:C--L:C = [{ext:N}, {ext:N}, {ext:N}, {ext:N}, {ext:N}]: (Prelude.IO.map [!{ext:N}, !{ext:N}, !{ext:N}])
|
||||
Prelude.IO.Applicative implementation at Prelude/IO.idr:L:C--L:C = []: (%con Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam b (%lam a (%lam func (%lam {arg:N} (%lam {eta:N} (Prelude.IO.map [!func, !{arg:N}, !{eta:N}])))))), (%lam a (%lam {arg:N} (%lam {eta:N} !{arg:N}))), (%lam b (%lam a (%lam {arg:N} (%lam {arg:N} (%lam {eta:N} (%let {act:N} (!{arg:N} [!{eta:N}]) (%let {act:N} (!{arg:N} [!{eta:N}]) (!{act:N} [!{act:N}]))))))))])
|
||||
Prelude.IO.<*> = [{arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (%let {act:N} (!{arg:N} [!{ext:N}]) (!{act:N} [!{act:N}])))
|
||||
|
||||
|
||||
@ -1,84 +1,32 @@
|
||||
Dumping case trees to Main.cases
|
||||
prim__add_Int = [{arg:N}, {arg:N}]: (+Int [!{arg:N}, !{arg:N}])
|
||||
prim__add_Integer = [{arg:N}, {arg:N}]: (+Integer [!{arg:N}, !{arg:N}])
|
||||
prim__sub_Int = [{arg:N}, {arg:N}]: (-Int [!{arg:N}, !{arg:N}])
|
||||
prim__sub_Integer = [{arg:N}, {arg:N}]: (-Integer [!{arg:N}, !{arg:N}])
|
||||
prim__mul_Int = [{arg:N}, {arg:N}]: (*Int [!{arg:N}, !{arg:N}])
|
||||
prim__mul_Integer = [{arg:N}, {arg:N}]: (*Integer [!{arg:N}, !{arg:N}])
|
||||
prim__div_Int = [{arg:N}, {arg:N}]: (/Int [!{arg:N}, !{arg:N}])
|
||||
prim__mod_Int = [{arg:N}, {arg:N}]: (%Int [!{arg:N}, !{arg:N}])
|
||||
prim__lt_Int = [{arg:N}, {arg:N}]: (<Int [!{arg:N}, !{arg:N}])
|
||||
prim__lte_Int = [{arg:N}, {arg:N}]: (<=Int [!{arg:N}, !{arg:N}])
|
||||
prim__lte_Integer = [{arg:N}, {arg:N}]: (<=Integer [!{arg:N}, !{arg:N}])
|
||||
prim__eq_Int = [{arg:N}, {arg:N}]: (==Int [!{arg:N}, !{arg:N}])
|
||||
prim__gte_Int = [{arg:N}, {arg:N}]: (>=Int [!{arg:N}, !{arg:N}])
|
||||
prim__gt_Int = [{arg:N}, {arg:N}]: (>Int [!{arg:N}, !{arg:N}])
|
||||
prim__believe_me = [{arg:N}, {arg:N}, {arg:N}]: (believe_me [!{arg:N}, !{arg:N}, !{arg:N}])
|
||||
prim__crash = [{arg:N}, {arg:N}]: (crash [!{arg:N}, !{arg:N}])
|
||||
prim__cast_IntegerInt = [{arg:N}]: (cast-Integer-Int [!{arg:N}])
|
||||
Main.main = [{ext:N}]: (Prelude.Interfaces.sum [(%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [!func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [!func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [!{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [!{i_con:N}, !funcM, !init, !input]))))))))]), (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [(%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
|
||||
Prelude.Basics.not = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1), (%constcase 1 0)] Nothing)
|
||||
Prelude.Basics.intToBool = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1)] Just 0)
|
||||
Prelude.Basics.flip = [{arg:N}, {arg:N}, {arg:N}]: ((!{arg:N} [!{arg:N}]) [!{arg:N}])
|
||||
Prelude.Basics.True = Constructor tag Just 0 arity 0
|
||||
Prelude.Basics.False = Constructor tag Just 1 arity 0
|
||||
Prelude.Basics.Bool = Constructor tag Nothing arity 0
|
||||
Prelude.Basics.&& = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%force Lazy !{arg:N})), (%constcase 1 1)] Nothing)
|
||||
Builtin.snd = [{arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
|
||||
Builtin.idris_crash = [{ext:N}]: (crash [___, !{ext:N}])
|
||||
Builtin.fst = [{arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
|
||||
Builtin.believe_me = [{ext:N}]: (believe_me [___, ___, !{ext:N}])
|
||||
Builtin.assert_total = [{arg:N}]: !{arg:N}
|
||||
Builtin.MkPair = Constructor tag Just 0 arity 2
|
||||
Prelude.Types.case block in rangeFromThen = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.countFrom [!{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))])), (%constcase 1 (Prelude.Types.countFrom [!{arg:N}, (%lam n (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!n]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))]))] Nothing)
|
||||
Prelude.Types.case block in case block in case block in rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.Nil Just 0 []))] Nothing)
|
||||
Prelude.Types.case block in case block in rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeBefore [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam n (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!n]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in case block in rangeFromThenTo [!{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}, (Prelude.Basics.&& [(%case (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing), (%delay Lazy (%case (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing))])]))] Nothing)
|
||||
Prelude.Types.case block in rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeBefore [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromThenTo [!{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)]))] Nothing)
|
||||
Prelude.Types.case block in case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam x (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!x]) [(%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])]))] Nothing)
|
||||
Prelude.Types.case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)
|
||||
Prelude.Types.case block in takeBefore = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.Nil Just 0 [])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (Prelude.Types.takeBefore [!{arg:N}, (%force Inf !{arg:N})])]))] Nothing)
|
||||
Prelude.Types.case block in takeUntil = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (Prelude.Types.takeUntil [!{arg:N}, (%force Inf !{arg:N})])]))] Nothing)
|
||||
Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [!{arg:N}])), (%constcase 1 0)] Nothing)
|
||||
Prelude.Types.rangeFrom = [{arg:N}, {arg:N}]: (Prelude.Types.countFrom [!{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [(%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]) [!{arg:N}]))] Nothing))])
|
||||
Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)])
|
||||
Prelude.Types.rangeFromThen = [{arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromThen [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)])
|
||||
Prelude.Types.rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromThenTo [!{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)])
|
||||
Prelude.Types.null = [{arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] (%delay Lazy 0)), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (%delay Lazy 1))] Nothing)
|
||||
Prelude.Types.foldr = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] ((!{arg:N} [!{e:N}]) [(Prelude.Types.foldr [!{arg:N}, !{arg:N}, !{e:N}])]))] Nothing)
|
||||
Prelude.Types.foldl = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (Prelude.Types.foldl [!{arg:N}, ((!{arg:N} [!{arg:N}]) [!{e:N}]), !{e:N}]))] Nothing)
|
||||
Prelude.Types.foldlM = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (Prelude.Types.foldl [(%lam ma (%lam b (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!ma]) [(%lam {eta:N} (Prelude.Basics.flip [!{arg:N}, !b, !{eta:N}]))]))] Nothing))), (%case (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{arg:N}]))] Nothing), !{ext:N}])
|
||||
Prelude.Types.Range at Prelude/Types.idr:L:C--L:C = Constructor tag Just 0 arity 4
|
||||
Prelude.Types.Range implementation at Prelude/Types.idr:L:C--L:C = [{arg:N}]: (%con Prelude.Types.Range at Prelude/Types.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromThenTo [!{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}])))), (%lam {arg:N} (Prelude.Types.rangeFrom [!{arg:N}, !{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromThen [!{arg:N}, !{arg:N}, !{arg:N}])))])
|
||||
Prelude.Types.Foldable implementation at Prelude/Types.idr:L:C--L:C = []: (%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [!func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [!func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [!{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [!{i_con:N}, !funcM, !init, !input]))))))))])
|
||||
Prelude.Types.takeUntil = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeUntil [!{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
|
||||
Prelude.Types.takeBefore = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeBefore [!{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
|
||||
Prelude.Types.rangeFromTo = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Types.Range at Prelude/Types.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.Types.prim__integerToNat = [{arg:N}]: (Prelude.Types.case block in prim__integerToNat [!{arg:N}, (%case (<=Integer [0, !{arg:N}]) [(%constcase 0 1)] Just 0)])
|
||||
Prelude.Types.countFrom = [{arg:N}, {arg:N}]: (%con Prelude.Types.Stream.:: Just 0 [!{arg:N}, (%delay Inf (Prelude.Types.countFrom [(!{arg:N} [!{arg:N}]), !{arg:N}]))])
|
||||
Prelude.Types.Z = Constructor tag Just 0 arity 0
|
||||
Prelude.Types.Stream.Stream = Constructor tag Nothing arity 1
|
||||
Prelude.Types.Nil = Constructor tag Just 0 arity 0
|
||||
Prelude.Types.:: = Constructor tag Just 1 arity 2
|
||||
Prelude.Types.Stream.:: = Constructor tag Just 0 arity 2
|
||||
Prelude.Num.case block in mod = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 1 (%Int [!{arg:N}, !{arg:N}]))] Just (Builtin.idris_crash ["Unhandled input for Prelude.Num.case block in mod at Prelude/Num.idr:L:C--L:C"]))
|
||||
Prelude.Num.case block in div = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 1 (/Int [!{arg:N}, !{arg:N}]))] Just (Builtin.idris_crash ["Unhandled input for Prelude.Num.case block in div at Prelude/Num.idr:L:C--L:C"]))
|
||||
Prelude.Num.negate = [{arg:N}]: (-Int [0, !{arg:N}])
|
||||
Prelude.Num.mod = [{arg:N}, {arg:N}]: (Prelude.Num.case block in mod [!{arg:N}, !{arg:N}, (Prelude.EqOrd.== [!{arg:N}, (cast-Integer-Int [0])])])
|
||||
Prelude.Num.fromInteger = [{ext:N}]: (cast-Integer-Int [!{ext:N}])
|
||||
Prelude.Num.div = [{arg:N}, {arg:N}]: (Prelude.Num.case block in div [!{arg:N}, !{arg:N}, (Prelude.EqOrd.== [!{arg:N}, (cast-Integer-Int [0])])])
|
||||
Prelude.Num.Num at Prelude/Num.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Num.Constraint (Num ty) = [{arg:N}]: (%case !{arg:N} [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing)
|
||||
Prelude.Num.Num implementation at Prelude/Num.idr:L:C--L:C = []: (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])
|
||||
Prelude.Num.Neg implementation at Prelude/Num.idr:L:C--L:C = []: (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])
|
||||
Prelude.Num.Integral implementation at Prelude/Num.idr:L:C--L:C = []: (%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))])
|
||||
Prelude.Num.- = [{ext:N}, {ext:N}]: (-Int [!{ext:N}, !{ext:N}])
|
||||
Prelude.Num.+ = [{ext:N}, {ext:N}]: (+Int [!{ext:N}, !{ext:N}])
|
||||
Prelude.Num.* = [{ext:N}, {ext:N}]: (*Int [!{ext:N}, !{ext:N}])
|
||||
Prelude.Num.fromInteger = [{arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [!{ext:N}]))] Nothing)
|
||||
Prelude.Num.- = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.Num.+ = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.EqOrd.case block in case block in compare = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 1), (%constcase 1 2)] Nothing)
|
||||
Prelude.EqOrd.case block in compare = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 0), (%constcase 1 (Prelude.EqOrd.case block in case block in compare [!{arg:N}, !{arg:N}, (Prelude.EqOrd.== [!{arg:N}, !{arg:N}])]))] Nothing)
|
||||
Prelude.EqOrd.case block in max = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 !{arg:N}), (%constcase 1 !{arg:N})] Nothing)
|
||||
@ -86,47 +34,15 @@ Prelude.EqOrd.case block in min = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [
|
||||
Prelude.EqOrd.min = [{arg:N}, {arg:N}]: (Prelude.EqOrd.case block in min [!{arg:N}, !{arg:N}, (Prelude.EqOrd.< [!{arg:N}, !{arg:N}])])
|
||||
Prelude.EqOrd.max = [{arg:N}, {arg:N}]: (Prelude.EqOrd.case block in max [!{arg:N}, !{arg:N}, (Prelude.EqOrd.> [!{arg:N}, !{arg:N}])])
|
||||
Prelude.EqOrd.compare = [{arg:N}, {arg:N}]: (Prelude.EqOrd.case block in compare [!{arg:N}, !{arg:N}, (Prelude.EqOrd.< [!{arg:N}, !{arg:N}])])
|
||||
Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C = Constructor tag Just 0 arity 8
|
||||
Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C = Constructor tag Just 0 arity 2
|
||||
Prelude.EqOrd.Constraint (Eq ty) = [{arg:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] !{e:N})] Nothing)
|
||||
Prelude.EqOrd.Ord implementation at Prelude/EqOrd.idr:L:C--L:C = []: (%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))])
|
||||
Prelude.EqOrd.Eq implementation at Prelude/EqOrd.idr:L:C--L:C = []: (%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))])
|
||||
Prelude.EqOrd.> = [{arg:N}, {arg:N}]: (%case (>Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.>= = [{arg:N}, {arg:N}]: (%case (>=Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.== = [{arg:N}, {arg:N}]: (%case (==Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.< = [{arg:N}, {arg:N}]: (%case (<Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.<= = [{arg:N}, {arg:N}]: (%case (<=Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd./= = [{arg:N}, {arg:N}]: (Prelude.Basics.not [(Prelude.EqOrd.== [!{arg:N}, !{arg:N}])])
|
||||
Prelude.EqOrd.LT = Constructor tag Just 0 arity 0
|
||||
Prelude.EqOrd.GT = Constructor tag Just 2 arity 0
|
||||
Prelude.EqOrd.EQ = Constructor tag Just 1 arity 0
|
||||
Prelude.EqOrd.>= = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.EqOrd.> = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.EqOrd.== = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.EqOrd.<= = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.EqOrd.< = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.Interfaces.Functor at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 2 (newtype by 1)
|
||||
Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 4
|
||||
Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Interfaces.Constraint (Applicative m) = [{arg:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing)
|
||||
Prelude.Interfaces.sum = [{arg:N}, {ext:N}]: (%case (Builtin.fst [!{arg:N}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {clam:N} (%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{clam:N}]))] Nothing)))]) [(%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
|
||||
Prelude.Interfaces.pure = [{arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{ext:N}]))] Nothing)
|
||||
Prelude.Interfaces.foldr = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]) [!{arg:N}])))] Nothing)
|
||||
Prelude.Interfaces.foldl = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]) [!{arg:N}])))] Nothing)
|
||||
Prelude.Interfaces.>>= = [{arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, !{arg:N}])
|
||||
PrimIO.case block in case block in io_bind = [{arg:N}, {arg:N}, {arg:N}]: (!{arg:N} [!{arg:N}])
|
||||
PrimIO.case block in io_bind = [{arg:N}, {arg:N}]: (PrimIO.case block in case block in io_bind [!{arg:N}, ___, (!{arg:N} [!{arg:N}])])
|
||||
PrimIO.unsafePerformIO = [{arg:N}]: (PrimIO.unsafeCreateWorld [(%lam w (PrimIO.case block in unsafePerformIO [!{arg:N}, (!{arg:N} [!w])]))])
|
||||
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}]: !{arg:N}
|
||||
PrimIO.unsafeCreateWorld = [{arg:N}]: (!{arg:N} [%MkWorld])
|
||||
PrimIO.io_pure = [{arg:N}, {ext:N}]: !{arg:N}
|
||||
PrimIO.io_bind = [{arg:N}, {arg:N}, {ext:N}]: (PrimIO.case block in io_bind [!{arg:N}, (!{arg:N} [!{ext:N}])])
|
||||
PrimIO.MkIORes = Constructor tag Just 0 arity 3 (newtype by 1)
|
||||
PrimIO.MkIO = Constructor tag Just 0 arity 2 (newtype by 1)
|
||||
Prelude.IO.pure = [{arg:N}, {ext:N}]: !{arg:N}
|
||||
Prelude.IO.map = [{arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (!{arg:N} [!{act:N}]))
|
||||
Prelude.IO.Functor implementation at Prelude/IO.idr:L:C--L:C = [{ext:N}, {ext:N}, {ext:N}, {ext:N}, {ext:N}]: (Prelude.IO.map [!{ext:N}, !{ext:N}, !{ext:N}])
|
||||
Prelude.IO.Applicative implementation at Prelude/IO.idr:L:C--L:C = []: (%con Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam b (%lam a (%lam func (%lam {arg:N} (%lam {eta:N} (Prelude.IO.map [!func, !{arg:N}, !{eta:N}])))))), (%lam a (%lam {arg:N} (%lam {eta:N} !{arg:N}))), (%lam b (%lam a (%lam {arg:N} (%lam {arg:N} (%lam {eta:N} (%let {act:N} (!{arg:N} [!{eta:N}]) (%let {act:N} (!{arg:N} [!{eta:N}]) (!{act:N} [!{act:N}]))))))))])
|
||||
Prelude.IO.<*> = [{arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (%let {act:N} (!{arg:N} [!{ext:N}]) (!{act:N} [!{act:N}])))
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user