git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/test/interactive012/expected
33 lines 764 B history raw
1 x : Int
2--------------------------------------
3mkString_rhs_1 : String
4 x : String
5--------------------------------------
6mkString_rhs_2 : String
7--------------------------------------
8mkThing_rhs_1 : Int
9--------------------------------------
10mkThing_rhs_2 : String
11 str : Bool
12 x : IntString str
13--------------------------------------
14mkString2_rhs : String
15 x : ?what
16--------------------------------------
17mkString3_rhs_1 : String
18 x : ?what
19--------------------------------------
20mkString3_rhs_2 : String
21 a : Type
22 m : Nat
23 ys : Vect m a
24--------------------------------------
25append_rhs_1 : Vect m a
26 a : Type
27 x : a
28 m : Nat
29 ys : Vect m a
30 k : Nat
31 xs : Vect k a
32--------------------------------------
33append_rhs_2 : Vect (S (plus k m)) a