Given the expression of a term, we can try to directly match it, and there are helpers for this. But there is a smarter way using Lean's unification function isDefEq.

The function isDefEq takes two terms and returns a MetaM Bool. It returns true if the two terms are definitionally equal. More interestingly, if the terms have metavariables, it will try to solve them.

def leExpr? (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr)

Equations

• leExpr? e = match e.app4? `LE.le with | some (a, fst, b, c) => some (a, b, c) | x => none

def «command#leExpr[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

We will match in a smarted way:

• Create metavariables for the two terms, lhs and rhs.
• Create the expression lhs ≤ rhs.
• Equate this with the given expression and solve.
• Return the meta-variables.

def natLeExpr? (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Equations

• One or more equations did not get rendered due to their size.

def «command#natLeExpr_» : Lean.ParserDescr

Equations

• «command#natLeExpr_» = Lean.ParserDescr.node `«command#natLeExpr_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#natLeExpr") (Lean.ParserDescr.cat `term 0))

def «command#leExprAss[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

We will experiment with universe meta-levels. We will create a list [0] as List.cons 0 List.nil.

def termList_eg : Lean.ParserDescr

Equations

• termList_eg = Lean.ParserDescr.node `termList_eg 1024 (Lean.ParserDescr.symbol "list_eg")

def prodExpr? (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Equations

• One or more equations did not get rendered due to their size.

def «command#prodExpr[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.