on 7afa310 help sign in
Idris-dev/test/interactive006/interactive006.idr
3 lines 45 B history raw
1foo : Nat -> Nat -> Nat
2foo k j = ?foo_rhs1