Documentation

Lean.Meta.MatchUtil

@[inline]

def Lean.Meta.testHelper (e : Lean.Expr) (p : Lean.Expr → Lean.MetaM Bool) :

Lean.MetaM Bool

Equations

Lean.Meta.testHelper e p = do let a ← p e if a = true then pure true else do let a ← Lean.Meta.whnf e p a

@[inline]

def Lean.Meta.matchHelper? {α : Type} (e : Lean.Expr) (p? : Lean.Expr → Lean.MetaM (Option α)) :

Lean.MetaM (Option α)

Equations

Lean.Meta.matchHelper? e p? = do let a ← p? e match a with | none => do let a ← Lean.Meta.whnf e p? a | s => pure s

def Lean.Meta.matchEq? (e : Lean.Expr) :

Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Equations

Lean.Meta.matchEq? e = Lean.Meta.matchHelper? e fun e => pure (Lean.Expr.eq? e)

def Lean.Meta.matchHEq? (e : Lean.Expr) :

Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

Equations

Lean.Meta.matchHEq? e = Lean.Meta.matchHelper? e fun e => pure (Lean.Expr.heq? e)

def Lean.Meta.matchFalse (e : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.matchFalse e = Lean.Meta.testHelper e fun e => pure (Lean.Expr.isConstOf e `False)

def Lean.Meta.matchNot? (e : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.matchNot? e = Lean.Meta.matchHelper? e fun e => match Lean.Expr.not? e with | some e => pure (some e) | x => match Lean.Expr.arrow? e with | some (a, b) => do let a_1 ← Lean.Meta.matchFalse b if a_1 = true then pure (some a) else pure none | x => pure none

def Lean.Meta.matchNe? (e : Lean.Expr) :

Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Equations

Lean.Meta.matchNe? e = Lean.Meta.matchHelper? e fun e => match Lean.Expr.ne? e with | some r => pure (some r) | x => do let a ← Lean.Meta.matchNot? e match a with | some e => Lean.Meta.matchEq? e | x => pure none

def Lean.Meta.matchConstructorApp? (e : Lean.Expr) :

Lean.MetaM (Option Lean.ConstructorVal)

Equations

Lean.Meta.matchConstructorApp? e = do let env ← Lean.getEnv Lean.Meta.matchHelper? e fun e => pure (Lean.Expr.isConstructorApp? env e)