Char/String builtins for the Lurk Transpiler

argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel

MIT License

121 stars 9 forks source link

Char/String builtins for the Lurk Transpiler #193

Closed winston-h-zhang closed 2 years ago

winston-h-zhang commented 2 years ago

Closes #171.

Adds a bunch of functions in LurkFunctions.lean
We can now transpile things like "abc" ++ "def" and it will evaluate correctly.
~~TODO: Add the num and char special functions to our interpreter.~~ To be done in later PR
~~TODO: Similar builtins for UInt32 and Fin.~~ To be done in later PR
Seal off more core API for String and List, wherever we can be way more efficient

We can now move on to greater heights!

winston-h-zhang commented 2 years ago

Apologies as this is not the cleanest PR... but essentially the most important bit is in LurkFunctions.lean and Transpiler.lean; everything else is sort of collateral damage from me trying to fix bugs/test things/just other stuff.