Term elaborators have access to the expected type and to the local context.
This can be used to create a term analogue of the assumption tactic.
The first step is to access the local context using getLocalHyps.
It returns the context with the outermost bindings on the left, so it is traversed in reverse order.
For each local assumption, a type is inferred with Meta.inferType.
If it can be equal to the expected type, then the assumption is returned; if no assumption is suitable, then an error is produced.
syntax "anything!" : term
elab_rules <= expected
| `(anything!) => do
let hyps ← getLocalHyps
for h in hyps.reverse do
let t ← Meta.inferType h
if (← Meta.isDefEq t expected) then return h
throwError m!"No assumption in {hyps} has type {expected}"
The new syntax finds the function's bound variable:
7#eval (fun (n : Nat) => 2 + anything!) 5
7
It chooses the most recent suitable variable, as desired:
"It was y"#eval
let x := "x"
let y := "y"
"It was " ++ y
"It was y"
When no assumption is suitable, it returns an error that describes the attempt:
#eval
let x := Nat.zero
let y := "hello"
fun (f : Nat → Nat) =>
(No assumption in [x, y, f] has type Int → Intanything! : Int → Int)
No assumption in [x, y, f] has type Int → Int
Because it uses unification, the natural number literal is chosen here, because numeric literals may have any type with an OfNat instance.
Unfortunately, there is no OfNat instance for functions, so instance synthesis later fails.
#eval
let x := failed to synthesize
OfNat (Int → Int) 5
numerals are polymorphic in Lean, but the numeral `5` cannot be used in a context where the expected type is
Int → Int
due to the absence of the instance above
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.5
let y := "hello"
(anything! : Int → Int)
failed to synthesize
OfNat (Int → Int) 5
numerals are polymorphic in Lean, but the numeral `5` cannot be used in a context where the expected type is
Int → Int
due to the absence of the instance above
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
