Removed outdated comments
This commit is contained in:
parent
4ef32ff3fa
commit
b0a5f3fc09
|
@ -22,16 +22,4 @@
|
||||||
(match n
|
(match n
|
||||||
[z (some A a)]
|
[z (some A a)]
|
||||||
[(s (n-1 : Nat))
|
[(s (n-1 : Nat))
|
||||||
((recur rest) n-1)]))])
|
((recur rest) n-1)]))]))
|
||||||
#;(elim
|
|
||||||
List
|
|
||||||
Type
|
|
||||||
(lambda (A : Type) (ls : (List A))
|
|
||||||
(-> Nat (Maybe A)))
|
|
||||||
(lambda (A : Type) (n : Nat) (none A))
|
|
||||||
(lambda (A : Type) (a : A) (ls : (List A)) (ih : (-> Nat (Maybe A)))
|
|
||||||
(lambda (n : Nat)
|
|
||||||
(match n
|
|
||||||
[z (some A a)]
|
|
||||||
[(s (n-1 : Nat))
|
|
||||||
(ih n-1)])))))
|
|
||||||
|
|
|
@ -28,9 +28,7 @@
|
||||||
(only-in "../cur.rkt"
|
(only-in "../cur.rkt"
|
||||||
[elim real-elim]
|
[elim real-elim]
|
||||||
[#%app real-app]
|
[#%app real-app]
|
||||||
;; Somehow, using real-lambda instead of _lambda causes weird import error
|
|
||||||
[lambda real-lambda]
|
[lambda real-lambda]
|
||||||
#;[forall real-forall]
|
|
||||||
[define real-define]))
|
[define real-define]))
|
||||||
|
|
||||||
(begin-for-syntax
|
(begin-for-syntax
|
||||||
|
|
Loading…
Reference in New Issue
Block a user