funProp environment extension that stores all registered function properties

structure Mathlib.Meta.FunProp.FunPropDecl : Type

Basic information about function property

To use funProp to prove a function property P : (α→β)→Prop one has to provide FunPropDecl.

• funPropName : Lean.Name

  function transformation name

• path : Array Lean.Meta.DiscrTree.Key

  path for discriminatory tree

• funArgId : Nat

  argument index of a function this function property talks about. For example, this would be 4 for @Continuous α β _ _ f

• dischargeStx? : Option (Lean.TSyntax `tactic)

  Custom discharger for this function property.

instance Mathlib.Meta.FunProp.instInhabitedFunPropDecl : Inhabited Mathlib.Meta.FunProp.FunPropDecl

Equations

• Mathlib.Meta.FunProp.instInhabitedFunPropDecl = { default := { funPropName := default, path := default, funArgId := default, dischargeStx? := default } }

instance Mathlib.Meta.FunProp.instBEqFunPropDecl : BEq Mathlib.Meta.FunProp.FunPropDecl

Equations

• Mathlib.Meta.FunProp.instBEqFunPropDecl = { beq := Mathlib.Meta.FunProp.beqFunPropDecl✝ }

structure Mathlib.Meta.FunProp.FunPropDecls : Type

• decls : Lean.Meta.DiscrTree Mathlib.Meta.FunProp.FunPropDecl

  discriminatory tree for function properties

instance Mathlib.Meta.FunProp.instInhabitedFunPropDecls : Inhabited Mathlib.Meta.FunProp.FunPropDecls

Equations

• Mathlib.Meta.FunProp.instInhabitedFunPropDecls = { default := { decls := default } }

@[inline, reducible]

abbrev Mathlib.Meta.FunProp.FunPropDeclsExt : Type

Equations

• Mathlib.Meta.FunProp.FunPropDeclsExt = Lean.SimpleScopedEnvExtension Mathlib.Meta.FunProp.FunPropDecl Mathlib.Meta.FunProp.FunPropDecls

opaque Mathlib.Meta.FunProp.funPropDeclsExt : Mathlib.Meta.FunProp.FunPropDeclsExt

def Mathlib.Meta.FunProp.addFunPropDecl (declName : Lean.Name) (dischargeStx? : Option (Lean.TSyntax `tactic)) : Lean.MetaM Unit

Equations

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

def Mathlib.Meta.FunProp.getFunProp? (e : Lean.Expr) : Lean.MetaM (Option (Mathlib.Meta.FunProp.FunPropDecl × Lean.Expr))

Equations

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

def Mathlib.Meta.FunProp.isFunProp (e : Lean.Expr) : Lean.MetaM Bool

Equations

• Mathlib.Meta.FunProp.isFunProp e = do let __do_lift ← Mathlib.Meta.FunProp.getFunProp? e pure (Option.isSome __do_lift)

def Mathlib.Meta.FunProp.getFunPropDecl? (e : Lean.Expr) : Lean.MetaM (Option Mathlib.Meta.FunProp.FunPropDecl)

Returns function property declaration from e = P f.

Equations

• Mathlib.Meta.FunProp.getFunPropDecl? e = do let __do_lift ← Mathlib.Meta.FunProp.getFunProp? e match __do_lift with | some (decl, snd) => pure (some decl) | none => pure none

def Mathlib.Meta.FunProp.getFunPropFun? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Returns function f from e = P f and P is function property.

Equations

• Mathlib.Meta.FunProp.getFunPropFun? e = do let __do_lift ← Mathlib.Meta.FunProp.getFunProp? e match __do_lift with | some (fst, f) => pure (some f) | none => pure none

def Mathlib.Meta.FunProp.tacticToDischarge (tacticCode : Lean.TSyntax `tactic) : Lean.Expr → Lean.MetaM (Option Lean.Expr)

Equations

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

def Mathlib.Meta.FunProp.FunPropDecl.discharger (funPropDecl : Mathlib.Meta.FunProp.FunPropDecl) (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

• Mathlib.Meta.FunProp.FunPropDecl.discharger funPropDecl e = match funPropDecl.dischargeStx? with | some stx => Mathlib.Meta.FunProp.tacticToDischarge stx e | x => pure none