Wired program type checked.

[molikto]

test1 (t: nat): U = nat

test2 (a: nat): U = 
    (test1 a)
   where
    a: (test2 zero) = zero

An equivalent program doesn't type check in Coq

[coquand]

Thanks for the example.

I am not sure it should type-check however. The type-checking of a recursive definition

x : A = t

should be

x : A |- t : A (1)

For simplifying the implementation of HIT, we changed this to

x : A = t |- t : A (2)

but we have to think more which one (1) or (2) should be used for recursive definitions.

On 31 Aug 2016, at 06:37, Minghao Liu [email protected] wrote:

test1 (t: nat): U = nat

test2 (a: nat): U = (test1 a) where a: (test2 zero) = zero An equivalent problem doesn't type check in Coq

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/mortberg/cubicaltt/issues/51, or mute the thread https://github.com/notifications/unsubscribe-auth/ACrXlGOiACeU7LY5V7eyFNySjW8sFqa1ks5qlQT6gaJpZM4JxOSM.