3ce14c3871
Moved all curnel code into curnel/, and split the two kernel modules into separate files. Now the trusted core and the module/#lang stuff are in separate files. The #lang is now reprovided by "cur.rkt", which should also provide core agnostic sugar.
21 lines
515 B
Racket
21 lines
515 B
Racket
#lang s-exp "../cur.rkt"
|
|
(provide bool btrue bfalse if bnot)
|
|
|
|
(data bool : Type
|
|
(btrue : bool)
|
|
(bfalse : bool))
|
|
|
|
(define-syntax (if syn)
|
|
(syntax-case syn ()
|
|
[(_ t s f)
|
|
;; Compute the motive
|
|
(let ([M #`(lambda (x : #,(type-infer/syn #'t))
|
|
#,(type-infer/syn #'s))])
|
|
(quasisyntax/loc syn (elim bool t #,M s f)))]))
|
|
|
|
(define (bnot (x : bool)) (if x bfalse btrue))
|
|
(module+ test
|
|
(require rackunit)
|
|
(check-equal? (bnot btrue) bfalse)
|
|
(check-equal? (bnot bfalse) btrue))
|