A simple-ish Pure Type System simulator inspired by Ben Lynn's lambda calculus vending machine
- Haskell 93.5%
- Raku 6.5%
| app | test: Remove golden files and fix a very minor error | |
| examples | refactor: Add test suite and fix some warnings | |
| extra/micro-syntax | feat: Comment support, micro highlighters | |
| test | test: Remove golden files and fix a very minor error | |
| .gitignore | feat!: Full code parser | |
| LICENSE | chore: Scaffolding and main idea | |
| PTS.cabal | fix: Pattern matching | |
| README.md | docs: README | |
| rw-rules-axioms.md | docs: Rewriting rules for axioms implementation plan | |
PTS
A variant of Ben Lynn's lambda calculus vending machine that I eventually intend to augment with row types.
The type checking may be incomplete in some cases, as mentioned in Ben's blog post.
Check the examples/ directory for examples of Pure Type Systems and code using them.