Lean.Util.Recognizers

source

@[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 x => some (n, us) | x => none

source

@[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

source

@[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

source

@[inline]

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

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

Equations

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

source

@[inline]

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

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

Equations

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

source

@[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

source

@[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

source

@[inline]

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

Option (Lean.Expr × Lean.Expr)

Equations

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

source

@[inline]

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

Option Lean.Expr

Equations

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

source

@[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

source

@[inline]

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

Option (Lean.Expr × Lean.Expr)

Equations

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

source

@[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

source

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

Option (Lean.Expr × Lean.Expr)

Equations

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

source

@[inline]

def Lean.Expr.arrow? :

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

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

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

Option (Lean.Expr × List Lean.Expr)

Equations

Lean.Expr.listLit? e = (fun loop => loop e []) Lean.Expr.listLit?.loop

source

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

Option (Lean.Expr × List Lean.Expr)

source

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

Option (Lean.Expr × List Lean.Expr)

Equations

Lean.Expr.arrayLit? e = match Lean.Expr.app2? e `List.toArray with | some (x, e) => Lean.Expr.listLit? e | none => none

source

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

Option (Lean.Expr × Lean.Expr)

Equations

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

source

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

Option Lean.ConstructorVal

Equations

Lean.Expr.isConstructorApp? env e = match e with | Lean.Expr.lit (Lean.Literal.natVal n) x => if (n == 0) = true then Lean.Expr.getConstructorVal? env `Nat.zero else Lean.Expr.getConstructorVal? env `Nat.succ | x => match Lean.Expr.getAppFn e with | Lean.Expr.const n x x_1 => match Lean.Expr.getConstructorVal? env n with | some v => if (v.numParams + v.numFields == Lean.Expr.getAppNumArgs e) = true then some v else none | none => none | x => none

source

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

Bool

Equations

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

source

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

Option (Lean.ConstructorVal × Array Lean.Expr)

Equations

Lean.Expr.constructorApp? env e = OptionM.run (match e with | Lean.Expr.lit (Lean.Literal.natVal n) x => if (n == 0) = true then do let v ← Lean.Expr.getConstructorVal? env `Nat.zero pure (v, #[]) else do let v ← Lean.Expr.getConstructorVal? env `Nat.succ pure (v, #[Lean.mkNatLit (n - 1)]) | x => match Lean.Expr.getAppFn e with | Lean.Expr.const n x x_1 => do let v ← Lean.Expr.getConstructorVal? env n if (v.numParams + v.numFields == Lean.Expr.getAppNumArgs e) = true then pure (v, Lean.Expr.getAppArgs e) else none | x => none)