[work in progress]

highscript is a LEAN DSL that compiles to HVM code

features:

• 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)

installation

• install L∃∀N

• clone this repo

• run setup.sh

usage

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