Documentation

Lean.Util.Recognizers

@[inline]

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

Option (Lean.Name × List Lean.Level)

Equations

Lean.Expr.const? e = match e with | Lean.Expr.const n us a => some (n, us) | x => none

@[inline]

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

Option Lean.Expr

Equations

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

@[inline]

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

Option (Lean.Expr × Lean.Expr)

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

Lean.Expr.eq? p = Lean.Expr.app3? p `Eq

@[inline]

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

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

Equations

Lean.Expr.ne? p = Lean.Expr.app3? p `Ne

@[inline]

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

Option (Lean.Expr × Lean.Expr)

Equations

Lean.Expr.iff? p = Lean.Expr.app2? p `Iff

@[inline]

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

Option Lean.Expr

Equations

Lean.Expr.not? p = Lean.Expr.app1? p `Not

@[inline]

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

Option Lean.Expr

Equations

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

@[inline]

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

Option (Lean.Expr × Lean.Expr)

Equations

Lean.Expr.and? p = Lean.Expr.app2? p `And

@[inline]

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

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

Equations

Lean.Expr.heq? p = Lean.Expr.app4? p `HEq

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

Option (Lean.Expr × Lean.Expr)

Equations

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

@[inline]

def Lean.Expr.arrow?:

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

Equations

Lean.Expr.arrow? _fun_discr = match _fun_discr with | Lean.Expr.forallE a α β a_1 => if Lean.Expr.hasLooseBVars β = true then none else some (α, β) | x => none

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

Equations

Lean.Expr.isEq e = Lean.Expr.isAppOfArity e `Eq 3

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

Equations

Lean.Expr.isHEq e = Lean.Expr.isAppOfArity e `HEq 4

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

Equations

Lean.Expr.isIte e = Lean.Expr.isAppOfArity e `ite 5

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

Equations

Lean.Expr.isDIte e = Lean.Expr.isAppOfArity e `dite 5

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

Option (Lean.Expr × List Lean.Expr)

Equations

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

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

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

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

Option (Lean.Expr × Lean.Expr)

Recognize α × β

Equations

Lean.Expr.prod? e = Lean.Expr.app2? e `Prod

def Lean.Expr.isConstructorApp? (env : Lean.Environment) (e : Lean.Expr) :

Option Lean.ConstructorVal

Equations

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

def Lean.Expr.isConstructorApp (env : Lean.Environment) (e : Lean.Expr) :

Equations

Lean.Expr.isConstructorApp env e = Option.isSome (Lean.Expr.isConstructorApp? env e)

def Lean.Expr.constructorApp? (env : Lean.Environment) (e : Lean.Expr) :

Option (Lean.ConstructorVal × Array Lean.Expr)

Equations

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