We use interaction trees in order to represent imperative programs. Currently this is a shallow embedding, with a Boogie DSL elaborating directly to ITrees.
boogie-org/lean-embedding
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
| Name | Name | Last commit date | ||
|---|---|---|---|---|