Unary and binary natural numbers.

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

Apache License 2.0

204 stars 12 forks source link

Unary and binary natural numbers. #456

Closed cangiuli closed 5 years ago

cangiuli commented 5 years ago

I'm moving this out of #422. The representation is wrong, because nil and cons0 nil are both zero. Anyone (@ecavallo ?) is welcome to hack on this, but if nobody else does I'll eventually get back to it.

clayrat commented 5 years ago

In Coq and https://github.com/sbp/idris-bi they use 1 as a base constructor, and then construct nats and ints separately on top of that.

cangiuli commented 5 years ago

OMG!! I should open PRs with broken code more often! Thank you @favonia!