search

anoma / geb

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

Add type-inferencing for STLC terms. #88

Closed agureev closed 1 year ago

agureev commented 1 year ago

1) Move from structures to classes for STLC term definition 2) Remove and keep only minimally needed typing info for constructors 3) Add in type-inferencing for STLC terms 4) Add well-definedness predicate for terms in context 5) Amend the translation function in light of these changes

TODO: Type annotations for terms rather than explicit typing

However even with these changes it seems to solve issue #77

mariari commented 1 year ago

With the last commit, the code still errors on testing, but can be loaded from a fresh system