Closed wilbowma closed 7 years ago
See branch sigma. Compare our implementation of check-method https://github.com/wilbowma/cur/blob/master/cur-lib/cur/curnel/racket-impl/type-check.rkt#L569 to Type of branches from CIC (https://coq.inria.fr/distrib/current/refman/Reference-Manual006.html).
sigma
check-method
Type of branches
Basically, by trying to cheat and not threading through the canonical form, we screw up typing when using dependent elimination
See branch
sigma
. Compare our implementation ofcheck-method
https://github.com/wilbowma/cur/blob/master/cur-lib/cur/curnel/racket-impl/type-check.rkt#L569 toType of branches
from CIC (https://coq.inria.fr/distrib/current/refman/Reference-Manual006.html).Basically, by trying to cheat and not threading through the canonical form, we screw up typing when using dependent elimination