HepLean Documentation

Lean.Util.Recognizers

@[inline]

def Lean.Expr.const? (e : Lean.Expr) :

Option (Lake.Name × List Lean.Level)

Equations

(Lean.Expr.const n us).const? = some (n, us)
e.const? = none

Instances For

@[inline]

def Lean.Expr.app1? (e : Lean.Expr) (fName : Lake.Name) :

Option Lean.Expr

Equations

e.app1? fName = if e.isAppOfArity fName 1 = true then some e.appArg! else none

Instances For

@[inline]

def Lean.Expr.app2? (e : Lean.Expr) (fName : Lake.Name) :

Option (Lean.Expr × Lean.Expr)

Equations

e.app2? fName = if e.isAppOfArity fName 2 = true then some (e.appFn!.appArg!, e.appArg!) else none

Instances For

@[inline]

def Lean.Expr.app3? (e : Lean.Expr) (fName : Lake.Name) :

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

Equations

e.app3? fName = if e.isAppOfArity fName 3 = true then some (e.appFn!.appFn!.appArg!, e.appFn!.appArg!, e.appArg!) else none

Instances For

@[inline]

def Lean.Expr.app4? (e : Lean.Expr) (fName : Lake.Name) :

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

Equations

e.app4? fName = if e.isAppOfArity fName 4 = true then some (e.appFn!.appFn!.appFn!.appArg!, e.appFn!.appFn!.appArg!, e.appFn!.appArg!, e.appArg!) else none

Instances For

@[inline]

def Lean.Expr.eq? (p : Lean.Expr) :

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

Equations

p.eq? = p.app3? `Eq

Instances For

@[inline]

def Lean.Expr.ne? (p : Lean.Expr) :

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

Equations

p.ne? = p.app3? `Ne

Instances For

@[inline]

def Lean.Expr.iff? (p : Lean.Expr) :

Option (Lean.Expr × Lean.Expr)

Equations

p.iff? = p.app2? `Iff

Instances For

@[inline]

def Lean.Expr.eqOrIff? (p : Lean.Expr) :

Option (Lean.Expr × Lean.Expr)

Equations

p.eqOrIff? = match p.app3? `Eq with | some (fst, lhs, rhs) => some (lhs, rhs) | x => p.iff?

Instances For

@[inline]

def Lean.Expr.not? (p : Lean.Expr) :

Option Lean.Expr

Equations

p.not? = p.app1? `Not

Instances For

@[inline]

def Lean.Expr.notNot? (p : Lean.Expr) :

Option Lean.Expr

Equations

p.notNot? = match p.not? with | some p => p.not? | none => none

Instances For

@[inline]

def Lean.Expr.and? (p : Lean.Expr) :

Option (Lean.Expr × Lean.Expr)

Equations

p.and? = p.app2? `And

Instances For

@[inline]

def Lean.Expr.heq? (p : Lean.Expr) :

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

Equations

p.heq? = p.app4? `HEq

Instances For

def Lean.Expr.natAdd? (e : Lean.Expr) :

Option (Lean.Expr × Lean.Expr)

Equations

e.natAdd? = e.app2? `Nat.add

Instances For

@[inline]

def Lean.Expr.arrow? :

Lean.Expr → Option (Lean.Expr × Lean.Expr)

Equations

(Lean.Expr.forallE binderName α β binderInfo).arrow? = if β.hasLooseBVars = true then none else some (α, β)
x.arrow? = none

Instances For

def Lean.Expr.isEq (e : Lean.Expr) :

Equations

e.isEq = e.isAppOfArity `Eq 3

Instances For

def Lean.Expr.isHEq (e : Lean.Expr) :

Equations

e.isHEq = e.isAppOfArity `HEq 4

Instances For

def Lean.Expr.isIte (e : Lean.Expr) :

Equations

e.isIte = e.isAppOfArity `ite 5

Instances For

def Lean.Expr.isDIte (e : Lean.Expr) :

Equations

e.isDIte = e.isAppOfArity `dite 5

Instances For

def Lean.Expr.listLit? (e : Lean.Expr) :

Option (Lean.Expr × List Lean.Expr)

Equations

e.listLit? = Lean.Expr.listLit?.loop e []

Instances For

partial def Lean.Expr.listLit?.loop (e : Lean.Expr) (acc : List Lean.Expr) :

Option (Lean.Expr × List Lean.Expr)

def Lean.Expr.arrayLit? (e : Lean.Expr) :

Option (Lean.Expr × List Lean.Expr)

Equations

e.arrayLit? = if e.isAppOfArity' `List.toArray 2 = true then e.appArg!'.listLit? else none

Instances For

def Lean.Expr.prod? (e : Lean.Expr) :

Option (Lean.Expr × Lean.Expr)

Recognize α × β

Equations

e.prod? = e.app2? `Prod

Instances For