mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
26 lines
1.1 KiB
Lean4
26 lines
1.1 KiB
Lean4
def f1 {α} [ToString α] (a : α) : String := -- works
|
||
">> " ++ toString a
|
||
|
||
-- Moving `{α} [ToString α]` to a `variables` break the example
|
||
variable {α} [ToString α]
|
||
def f2 (a : α) : String :=
|
||
">> " ++ toString a
|
||
|
||
class Dummy (α : Type) := (val : α)
|
||
|
||
/- The following fails because `variables {α : Type _} [Dummy α]` is processed as `variable {α : Type _} variable [Dummy α]`
|
||
The first command elaborates `α` as `variable {α : Type u_1}` where `u_1` is a fresh metavariable.
|
||
That is, in Lean3, metavariables are resolved before the end of the command. -/
|
||
variable {α : Type _} [Dummy α]
|
||
|
||
def f3 {α : Type _} [Dummy α] : α := -- works
|
||
Dummy.val α
|
||
|
||
/-
|
||
In Lean4, we should use a different approach. We keep a metavariable context in the command elaborator.
|
||
Before, a declaration `D` is sent to the kernel we resolve the metavariables occurring in `D`.
|
||
We must implement a MetavarContext GC to make sure the metavariable context does not keep increasing.
|
||
That is, after a declaration is sent to the kernel, we visit all variables in the elaborator context and
|
||
instantiate assigned metavariables. Then, we delete all assigned metavariables.
|
||
-/
|