git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/interactive012/interactive012.idr
26 lines 713 B history raw
1IntString : Bool -> Type
2IntString False = Int
3IntString True = String
5mkString : (str : Bool) -> IntString str -> String
6mkString False x = ?mkString_rhs_1
7mkString True x = ?mkString_rhs_2
9mkThing : (str : Bool) -> IntString str
10mkThing False = ?mkThing_rhs_1
11mkThing True = ?mkThing_rhs_2
13mkString2 : (str : Bool) -> IntString str -> String
14mkString2 str x = ?mkString2_rhs
16mkString3 : (str : Bool) -> ?what -> String
17mkString3 False x = ?mkString3_rhs_1
18mkString3 True x = ?mkString3_rhs_2
20data Vect : Nat -> Type -> Type where
21 Nil : Vect Z a
22 (::) : a -> Vect k a -> Vect (S k) a
24append : Vect n a -> Vect m a -> Vect (n + m) a
25append [] ys = ?append_rhs_1
26append (x :: xs) ys = ?append_rhs_2