[work in progress]
highscript is a LEAN DSL that compiles to HVM code
- generate HVM
- standart lambda syntax
- simple type system
- linearize variables
- run HVM output
- support for custom ADT's
- Pattern matching
- multi target ADT's (like tagged Union)
-
install L∃∀N
-
clone this repo
-
run
setup.sh
see examples folder
after successfull installation it should be possible to import HighScript in lean file and run script on HVM backend with runHVM command
To run example which generates and runs HVM code
lean --run examples/fun_call.lean