A library for writing Lean IR as Lean syntax.
Example
noncomputable def myAdd (m n : Nat) : Nat :=
m + n
ir_impl myAdd (m : @& obj) (n : @& obj) :=
let x := Nat.add m n
ret x
#eval myAdd 1 2 -- 3-
Notifications
You must be signed in to change notification settings - Fork 0
Lean IR as Lean syntax
License
tydeu/lyre
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Lean IR as Lean syntax
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published