underscore symbol

Stream: new members

[rzeta0]

Quick question: Is the underscore symbol _ ever used anywhere other than the LHS of a relation statement?

And following on from that, does it "unify" only with the RHS of the most recent statement parsed?

(I can't find documentation describing what it does)

[Yaël Dillies]

Yes, it is generally a placeholder to be filled in by unification, eg

theorem foo (n : Nat) : n = n := rfl
example : 37 = 37 := foo _

[rzeta0]

That example is too advanced for me :)

Why does the _ in example : 37 = 37 := foo _ unify with?

[Kyle Miller]

foo _ is foo ?m for a fresh metavariable ?m. The type of foo ?m is ?m = ?m. This gets unified with 37 = 37, and the solution is ?m := 37. So, foo _ ends up being foo 37.

[Kyle Miller]

A "metavariable" is a hole in an expression that needs to be filled in at some point, and one of the side effects of unification is assigning expressions to metavariables. Unification is a general idea, and if you see "isDefEq" that's Lean's algorithm for both checking that two expressions are defeq and for trying to make them defeq by assigning to metavariables as necessary.