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

Merge branch 'master' into actual-inductives

Browse Source
This commit is contained in:
William J. Bowman 2015-03-24 20:14:00 -04:00
commit f5d387b689
1 changed files with 1 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
redex-curnel.rkt
View File

@ -50,8 +50,7 @@
(check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))) (check-true (t? (term (λ (x_0 : (Unv 0)) x_0)))))
;; 'A' ;; 'A'
;; (Unv 0)s of Universes ;; Types of Universes
;; Replace with sub-typing
(define-judgment-form cicL (define-judgment-form cicL
#:mode (unv-ok I O) #:mode (unv-ok I O)
#:contract (unv-ok U U) #:contract (unv-ok U U)