search

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
571 stars 76 forks source link

Wired program type checked. #51

Open molikto opened 8 years ago

molikto commented 8 years ago 
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 commented 8 years ago

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 notifications@github.com 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.