on master help sign in
Idris-dev/test/basic018/basic018.idr
14 lines 170 B history raw
1import Data.Vect
3thing : Nat
4thing = 42
6foo : -- (thing : Nat) ->
7 Vect thing elem
9bar : {thing : Nat} ->
10 Vect thing elem
12test : thing = S 41
13test = Refl