search

gebner / hott3

HoTT in Lean 3
Apache License 2.0
75 stars 11 forks source link

make idp_rec_on a recursor #5

Closed fpvandoorn closed 7 years ago

fpvandoorn commented 7 years ago

Do you know why idp_rec_on [link] is not accepted as a recursor? The error is 

invalid user defined recursor, motive result sort must be Prop or Type.{l} where l is a universe parameter

but the motive result sort is Type u_2, so I think that should be fine.

PS: let me know if I'm opening too much of these issues or if you prefer another line of communication

gebner commented 7 years ago

This is an old error message from before we renamed Type to Sort. That is, it should read "Prop or Sort l". Changing the motive of transport and idp_rec_on to eliminate into Sort makes Lean accept it as a recursor.

I don't mind the issues.

fpvandoorn commented 7 years ago

Ah, that makes sense.

If I do that though, I get the deep recursion was detected at 'whnf' error message when applying idp_rec_on. It happens even without using the induction tactic, but it doesn't happen if idp_rec_on is not marked as recursor. See https://github.com/fpvandoorn/hott3/blob/idp_rec_on/init/pathover.lean#L217-L224

gebner commented 7 years ago

This is a bug in the VM compiler. It expects all auxiliary recursors to be reducible.

fpvandoorn commented 7 years ago

Thanks!