Add basic `quote` to the evaluator

argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel

MIT License

114 stars 8 forks source link

Closed winston-h-zhang closed 2 years ago

winston-h-zhang commented 2 years ago

Quality of life change so we don't have to keep writing cons everywhere to create explicit lists.

Refactored SExpr down to only two constructors: Literal and cons (for lisp like lists).
Moved Literals into their own file.
Removed .sexpr from Value and patched the .quote evaluate case.