From 1221fb5e41186853a3ea581ce055e69c4cdedde3 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Sun, 27 Sep 2015 13:26:23 -0400 Subject: [PATCH] (x v) etc should be a value form When x is a inductive constructor, (x v), and ((x v) v), and so on should be considered values. --- curnel/redex-core.rkt | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt index e97c7a5..f0c425c 100644 --- a/curnel/redex-core.rkt +++ b/curnel/redex-core.rkt @@ -35,7 +35,8 @@ (i ::= natural) (U ::= (Unv i)) (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))) (define x? (redex-match? cicL x)) @@ -62,7 +63,12 @@ (check-true (e? (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 + (v? (term (refl Nat)))) + (check-true + (v? (term ((refl Nat) z)))) + ) ;; 'A' ;; Types of Universes