anoma / geb

A Categorical View of Computation
https://anoma.github.io/geb/
GNU General Public License v3.0
28 stars 10 forks source link

Implementation of Natural Numbers #138

Closed agureev closed 1 year ago

agureev commented 1 year ago

1) Introduces SeqN category of finite natural number sequences

2) Introduces a new pipeline compiling STLC terms through SeqN instead of BITC

3) Implements for each n an object of natural numbers of n-bit length alongside appropriate floored operations alongside new API. Propagated the implementation to STLC and SeqN.

4) Implements is-less-than and is-equal-to predicates on natural numbers in Geb, propagates the change to STLC and SeqN.

5) Upgrades the pipeline now supporting compilation of STLC+Natural numbers+Natural Number Predicates to Vamp-IR