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 #51, or mute the thread https://github.com/notifications/unsubscribe-auth/ACrXlGOiACeU7LY5V7eyFNySjW8sFqa1ks5qlQT6gaJpZM4JxOSM.