aeneas

aeneas copied to clipboard

Namespaces in generated Lean code

1

In a certain sense there are two kinds of external definition - those from outside the crate being compiled, and those defined inside it. For consistency, I would expect that...

dylanede

Universe polymorphism in Lean backend

6

Currently, generic parameters are generated with sort `Type`, and much of the Lean backend library uses `Type` (but not all of it - I see `Type u` in quite a...

dylanede

Today we have two maintain two files for the Lean tutorial: this is an avoidable maintenance burden.

sonmarcho

The following fails: ```lean example (x : U32) : ∃ (x' : U32), ok x' = x := by progress ``` In the following the goal for the `else` branch...

sonmarcho