support for dependent types - Githubissues

nunchaku-inria / nunchaku

Model finder for higher-order logic

https://nunchaku-inria.github.io/nunchaku/

BSD 2-Clause "Simplified" License

42 stars 3 forks source link

support for dependent types #20

Open c-cube opened 7 years ago

c-cube commented 7 years ago

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