nunchaku icon indicating copy to clipboard operation
nunchaku copied to clipboard

Published 20 hours ago • verified publisher icon nunchaku-inria

support for dependent types

Open c-cube opened this issue 7 years ago • 0 comments

  • no universes
  • must be accepted in typechecking (without inference for term parameters)
  • do the encoding (hatt 2016)

c-cube avatar Jun 22 '17 09:06 c-cube