diff --git a/cur-lib/cur/curnel/hybrid-core.rkt b/cur-lib/cur/curnel/hybrid-core.rkt index ecdbbbc..177ff6a 100644 --- a/cur-lib/cur/curnel/hybrid-core.rkt +++ b/cur-lib/cur/curnel/hybrid-core.rkt @@ -558,6 +558,7 @@ (wf Δ (Γ x : t))] [(side-condition ,(not (empty-Δ? (term Δ_1)))) + ;; TODO: Depends on order, but "first" here is nondeterministic/unspecified (where x_D ,(dict-iterate-key (term Δ_1) (dict-iterate-first (term Δ_1)))) (where t_D (Δ-ref-type Δ_1 x_D)) (where (x_c ...) (Δ-ref-constructors Δ_1 x_D)) diff --git a/cur-test/cur/tests/hybrid-core.rkt b/cur-test/cur/tests/hybrid-core.rkt index 6a89fff..3bb117a 100644 --- a/cur-test/cur/tests/hybrid-core.rkt +++ b/cur-test/cur/tests/hybrid-core.rkt @@ -61,6 +61,7 @@ (nat (Unv 0) ()) (heap (Unv 0) ()) (pre (Π (temp808 : heap) (Unv 0)) ())))) +(displayln sigma) (check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (true (Unv 0) ((T : true))))))) (check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (false (Unv 0) ()))))) (check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (equal (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))