suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

(x v) etc should be a value form

Browse Source 
When x is a inductive constructor, (x v), and ((x v) v), and so on
should be considered values.
This commit is contained in:
William J. Bowman 2015-09-27 13:26:23 -04:00
parent 8aabbc219b
commit 1221fb5e41
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 8 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
curnel/redex-core.rkt
View File

@ -35,7 +35,8 @@
(i ::= natural) (i ::= natural)
(U ::= (Unv i)) (U ::= (Unv i))
(x ::= variable-not-otherwise-mentioned) (x ::= variable-not-otherwise-mentioned)
(v ::= (Π (x : t) t) (λ (x : t) t) elim x U) (v ::= (Π (x : t) t) (λ (x : t) t) elim x U capp)
(capp ::= (x v) (capp v))
(t e ::= v (t t))) (t e ::= v (t t)))
(define x? (redex-match? cicL x)) (define x? (redex-match? cicL x))
@ -62,7 +63,12 @@
(check-true (e? (term (λ (x_0 : (Unv 0)) x_0)))) (check-true (e? (term (λ (x_0 : (Unv 0)) x_0))))
(check-true (v? (term (λ (x_0 : (Unv 0)) x_0)))) (check-true (v? (term (λ (x_0 : (Unv 0)) x_0))))
(check-true (t? (term (λ (x_0 : (Unv 0)) x_0)))) (check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
(check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))) (check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
(check-true
(v? (term (refl Nat))))
(check-true
(v? (term ((refl Nat) z))))
)
;; 'A' ;; 'A'
;; Types of Universes ;; Types of Universes