structure Lean.Meta.Simp.Result : Type

The result of simplifying some expression e.

• expr : Expr

  The simplified version of e

• proof? : Option Expr

  A proof that $e = $expr, where the simplified expression is on the RHS. If none, the proof is assumed to be refl.

• cache : Bool

  If cache := true the result is cached. Warning: we will remove this field in the future. It is currently used by arith := true, but we can now refactor the code to avoid the hack.

Instances For

• Lean.Meta.Simp.instInhabitedResult

instance Lean.Meta.Simp.instInhabitedResult : Inhabited Result

Equations

• Lean.Meta.Simp.instInhabitedResult = { default := { expr := default, proof? := default, cache := default } }

def Lean.Meta.Simp.mkEqTransOptProofResult (h? : Option Expr) (cache : Bool) (r : Result) : MetaM Result

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Simp.mkEqTransOptProofResult none true r = pure r
• Lean.Meta.Simp.mkEqTransOptProofResult none false r = pure { expr := r.expr, proof? := r.proof?, cache := false }

def Lean.Meta.Simp.Result.mkEqTrans (r₁ r₂ : Result) : MetaM Result

Equations

• r₁.mkEqTrans r₂ = Lean.Meta.Simp.mkEqTransOptProofResult r₁.proof? r₁.cache r₂

def Lean.Meta.Simp.Result.mkEqSymm (e : Expr) (r : Result) : MetaM Result

Flip the proof in a Simp.Result.

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Simp.Cache : Type

Equations

• Lean.Meta.Simp.Cache = Lean.SExprMap Lean.Meta.Simp.Result

@[reducible, inline]

abbrev Lean.Meta.Simp.CongrCache : Type

Equations

• Lean.Meta.Simp.CongrCache = Lean.ExprMap (Option Lean.Meta.CongrTheorem)

structure Lean.Meta.Simp.Context : Type

• config : Config
• zetaDeltaSet : FVarIdSet

  Local declarations to propagate to Meta.Context

• initUsedZetaDelta : FVarIdSet

  When processing Simp arguments, zetaDelta may be performed if zetaDeltaSet is not empty. We save the local free variable ids in initUsedZetaDelta. initUsedZetaDelta is a subset of zetaDeltaSet.

• metaConfig : ConfigWithKey
• indexConfig : ConfigWithKey
• maxDischargeDepth : UInt32

  maxDischargeDepth from config as an UInt32.

• simpTheorems : SimpTheoremsArray
• congrTheorems : SimpCongrTheorems
• parent? : Option Expr

  Stores the "parent" term for the term being simplified. If a simplification procedure result depends on this value, then it is its reponsability to set Result.cache := false.

  Motivation for this field: Suppose we have a simplification procedure for normalizing arithmetic terms. Then, given a term such as t_1 + ... + t_n, we don't want to apply the procedure to every subterm t_1 + ... + t_i for i < n for performance issues. The procedure can accomplish this by checking whether the parent term is also an arithmetical expression and do nothing if it is. However, it should set Result.cache := false to ensure we don't miss simplification opportunities. For example, consider the following:

  example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
    simp_arith only
    ...
  

  If we don't set Result.cache := false for the first x + x, then we get the resulting state:

  ... |- id (2*x + y) = id (x + x)
  

  instead of

  ... |- id (2*x + y) = id (2*x)
  

  as expected.

  Remark: given an application f a b c the "parent" term for f, a, b, and c is f a b c.

• dischargeDepth : UInt32
• lctxInitIndices : Nat

  Number of indices in the local context when starting simp. We use this information to decide which assumptions we can use without invalidating the cache.

• inDSimp : Bool

  If inDSimp := true, then simp is in dsimp mode, and only applying transformations that presereve definitional equality.

Instances For

• Lean.Meta.Simp.instInhabitedContext

instance Lean.Meta.Simp.instInhabitedContext : Inhabited Context

Equations

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

def Lean.Meta.Simp.mkContext (config : Config := { maxSteps := defaultMaxSteps, maxDischargeDepth := 2, contextual := false, memoize := true, singlePass := false, zeta := true, beta := true, eta := true, etaStruct := EtaStructMode.all, iota := true, proj := true, decide := false, arith := false, autoUnfold := false, dsimp := true, failIfUnchanged := true, ground := false, unfoldPartialApp := false, zetaDelta := false, index := true, implicitDefEqProofs := true }) (simpTheorems : SimpTheoremsArray := ∅) (congrTheorems : SimpCongrTheorems := { lemmas := { stage₁ := true, map₁ := ∅, map₂ := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray } } }) : MetaM Context

Equations

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

def Lean.Meta.Simp.Context.setConfig (context : Context) (config : Config) : MetaM Context

Equations

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

def Lean.Meta.Simp.Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context

Equations

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

def Lean.Meta.Simp.Context.setLctxInitIndices (c : Context) : MetaM Context

Equations

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

def Lean.Meta.Simp.Context.setAutoUnfold (c : Context) : Context

Equations

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

def Lean.Meta.Simp.Context.setFailIfUnchanged (c : Context) (flag : Bool) : Context

Equations

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

def Lean.Meta.Simp.Context.setMemoize (c : Context) (flag : Bool) : Context

Equations

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

def Lean.Meta.Simp.Context.setZetaDeltaSet (c : Context) (zetaDeltaSet initUsedZetaDelta : FVarIdSet) : Context

Equations

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

def Lean.Meta.Simp.Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool

Equations

• ctx.isDeclToUnfold declName = ctx.simpTheorems.isDeclToUnfold declName

structure Lean.Meta.Simp.UsedSimps : Type

• map : PHashMap Origin Nat
• size : Nat

Instances For

• Lean.Meta.Simp.instInhabitedUsedSimps

instance Lean.Meta.Simp.instInhabitedUsedSimps : Inhabited UsedSimps

Equations

• Lean.Meta.Simp.instInhabitedUsedSimps = { default := { map := default, size := default } }

def Lean.Meta.Simp.UsedSimps.insert (s : UsedSimps) (thmId : Origin) : UsedSimps

Equations

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

def Lean.Meta.Simp.UsedSimps.toArray (s : UsedSimps) : Array Origin

Equations

• s.toArray = Array.map (fun (x : Lean.Meta.Origin × Nat) => x.fst) ((Lean.PersistentHashMap.toArray s.map).qsort fun (x1 x2 : Lean.Meta.Origin × Nat) => decide (x1.snd < x2.snd))

structure Lean.Meta.Simp.Diagnostics : Type

• usedThmCounter : PHashMap Origin Nat

  Number of times each simp theorem has been used/applied.

• triedThmCounter : PHashMap Origin Nat

  Number of times each simp theorem has been tried.

• congrThmCounter : PHashMap Name Nat

  Number of times each congr theorem has been tried.

• thmsWithBadKeys : PArray SimpTheorem

  When using Simp.Config.index := false, and set_option diagnostics true, for every theorem used by simp, we check whether the theorem would be also applied if index := true, and we store it here if it would not have been tried.

Instances For

• Lean.Meta.Simp.instInhabitedDiagnostics

instance Lean.Meta.Simp.instInhabitedDiagnostics : Inhabited Diagnostics

Equations

• Lean.Meta.Simp.instInhabitedDiagnostics = { default := { usedThmCounter := default, triedThmCounter := default, congrThmCounter := default, thmsWithBadKeys := default } }

structure Lean.Meta.Simp.State : Type

• cache : Cache
• congrCache : CongrCache
• usedTheorems : UsedSimps
• numSteps : Nat
• diag : Diagnostics

structure Lean.Meta.Simp.Stats : Type

• usedTheorems : UsedSimps
• diag : Diagnostics

Instances For

• Lean.Meta.Simp.instInhabitedStats

instance Lean.Meta.Simp.instInhabitedStats : Inhabited Stats

Equations

• Lean.Meta.Simp.instInhabitedStats = { default := { usedTheorems := default, diag := default } }

instance Lean.Meta.Simp.instNonemptyMethodsRef : Nonempty Lean.Meta.Simp.MethodsRef✝

@[reducible, inline]

abbrev Lean.Meta.Simp.SimpM (α : Type) : Type

Equations

• Lean.Meta.SimpM = ReaderT Lean.Meta.Simp.MethodsRef✝ (ReaderT Lean.Meta.Simp.Context (StateRefT' IO.RealWorld Lean.Meta.Simp.State Lean.MetaM))

Instances For

• Lean.Meta.Simp.instInhabitedSimpM

@[inline]

def Lean.Meta.Simp.withIncDischargeDepth {α : Type} : SimpM α → SimpM α

Equations

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

@[inline]

def Lean.Meta.Simp.withSimpTheorems {α : Type} (s : SimpTheoremsArray) : SimpM α → SimpM α

Equations

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

@[inline]

def Lean.Meta.Simp.withInDSimp {α : Type} : SimpM α → SimpM α

Equations

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

@[inline]

def Lean.Meta.Simp.withSimpIndexConfig {α : Type} (x : SimpM α) : SimpM α

Executes x using a MetaM configuration for indexing terms. It is inferred from Simp.Config. For example, if the user has set simp (config := { zeta := false }), isDefEq and whnf in MetaM should not perform zeta reduction.

Equations

• Lean.Meta.Simp.withSimpIndexConfig x = do let __do_lift ← readThe Lean.Meta.Simp.Context Lean.Meta.withConfigWithKey __do_lift.indexConfig x

@[inline]

def Lean.Meta.Simp.withSimpMetaConfig {α : Type} (x : SimpM α) : SimpM α

Executes x using a MetaM configuration for inferred from Simp.Config.

Equations

• Lean.Meta.Simp.withSimpMetaConfig x = do let __do_lift ← readThe Lean.Meta.Simp.Context Lean.Meta.withConfigWithKey __do_lift.metaConfig x

@[extern lean_simp]

opaque Lean.Meta.Simp.simp (e : Expr) : SimpM Result

@[extern lean_dsimp]

opaque Lean.Meta.Simp.dsimp (e : Expr) : SimpM Expr

@[inline]

def Lean.Meta.Simp.modifyDiag (f : Diagnostics → Diagnostics) : SimpM Unit

Equations

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

inductive Lean.Meta.Simp.Step : Type

Result type for a simplification procedure. We have pre and post simplification procedures.

• done (r : Result) : Step

  For pre procedures, it returns the result without visiting any subexpressions.

  For post procedures, it returns the result.

• visit (e : Result) : Step

  For pre procedures, the resulting expression is passed to pre again.

  For post procedures, the resulting expression is passed to pre again IF Simp.Config.singlePass := false and resulting expression is not equal to initial expression.

• continue (e? : Option Result := none) : Step

  For pre procedures, continue transformation by visiting subexpressions, and then executing post procedures.

  For post procedures, this is equivalent to returning visit.

Instances For

• Lean.Meta.Simp.instInhabitedStep

instance Lean.Meta.Simp.instInhabitedStep : Inhabited Step

Equations

• Lean.Meta.Simp.instInhabitedStep = { default := Lean.Meta.Simp.Step.done default }

@[reducible, inline]

abbrev Lean.Meta.Simp.Simproc : Type

A simplification procedure. Recall that we have pre and post procedures. See Step.

Equations

• Lean.Meta.Simp.Simproc = (Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step)

Instances For

• Lean.Meta.Simp.instAndThenSimproc

@[reducible, inline]

abbrev Lean.Meta.Simp.DStep : Type

Equations

• Lean.Meta.Simp.DStep = Lean.TransformStep

@[reducible, inline]

abbrev Lean.Meta.Simp.DSimproc : Type

Similar to Simproc, but resulting expression should be definitionally equal to the input one.

Equations

• Lean.Meta.Simp.DSimproc = (Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep)

Instances For

• Lean.Meta.Simp.instAndThenDSimproc

def Lean.TransformStep.toStep (s : TransformStep) : Meta.Simp.Step

Equations

• (Lean.TransformStep.done e).toStep = Lean.Meta.Simp.Step.done { expr := e, proof? := none, cache := true }
• (Lean.TransformStep.visit e).toStep = Lean.Meta.Simp.Step.visit { expr := e, proof? := none, cache := true }
• (Lean.TransformStep.continue (some e)).toStep = Lean.Meta.Simp.Step.continue (some { expr := e, proof? := none, cache := true })
• Lean.TransformStep.continue.toStep = Lean.Meta.Simp.Step.continue

def Lean.Meta.Simp.mkEqTransResultStep (r : Result) (s : Step) : MetaM Step

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Simp.mkEqTransResultStep r (Lean.Meta.Simp.Step.done r') = do let __do_lift ← Lean.Meta.Simp.mkEqTransOptProofResult r.proof? r.cache r' pure (Lean.Meta.Simp.Step.done __do_lift)
• Lean.Meta.Simp.mkEqTransResultStep r (Lean.Meta.Simp.Step.visit r') = do let __do_lift ← Lean.Meta.Simp.mkEqTransOptProofResult r.proof? r.cache r' pure (Lean.Meta.Simp.Step.visit __do_lift)
• Lean.Meta.Simp.mkEqTransResultStep r Lean.Meta.Simp.Step.continue = pure (Lean.Meta.Simp.Step.continue (some r))

@[always_inline]

def Lean.Meta.Simp.andThen (f g : Simproc) : Simproc

"Compose" the two given simplification procedures. We use the following semantics.

• If f produces done or visit, then return f's result.
• If f produces continue, then apply g to new expression returned by f.

See Simp.Step type.

Equations

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

instance Lean.Meta.Simp.instAndThenSimproc : AndThen Simproc

Equations

• Lean.Meta.Simp.instAndThenSimproc = { andThen := fun (s₁ : Lean.Meta.Simp.Simproc) (s₂ : Unit → Lean.Meta.Simp.Simproc) => Lean.Meta.Simp.andThen s₁ (s₂ ()) }

@[always_inline]

def Lean.Meta.Simp.dandThen (f g : DSimproc) : DSimproc

Equations

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

instance Lean.Meta.Simp.instAndThenDSimproc : AndThen DSimproc

Equations

• Lean.Meta.Simp.instAndThenDSimproc = { andThen := fun (s₁ : Lean.Meta.Simp.DSimproc) (s₂ : Unit → Lean.Meta.Simp.DSimproc) => Lean.Meta.Simp.dandThen s₁ (s₂ ()) }

structure Lean.Meta.Simp.SimprocOLeanEntry : Type

Simproc .olean entry.

• declName : Name

  Name of a declaration stored in the environment which has type Simproc.

• post : Bool
• keys : Array SimpTheoremKey

Instances For

• Lean.Meta.Simp.instInhabitedSimprocOLeanEntry

instance Lean.Meta.Simp.instInhabitedSimprocOLeanEntry : Inhabited SimprocOLeanEntry

Equations

• Lean.Meta.Simp.instInhabitedSimprocOLeanEntry = { default := { declName := default, post := default, keys := default } }

structure Lean.Meta.Simp.SimprocEntryextends Lean.Meta.Simp.SimprocOLeanEntry : Type

Simproc entry. It is the .olean entry plus the actual function.

• declName : Name
• post : Bool
• keys : Array SimpTheoremKey
• proc : Simproc ⊕ DSimproc

  Recall that we cannot store Simproc into .olean files because it is a closure. Given SimprocOLeanEntry.declName, we convert it into a Simproc by using the unsafe function evalConstCheck.

Instances For

• Lean.Meta.Simp.instBEqSimprocEntry
• Lean.Meta.Simp.instToFormatSimprocEntry

@[reducible, inline]

abbrev Lean.Meta.Simp.SimprocTree : Type

Equations

• Lean.Meta.Simp.SimprocTree = Lean.Meta.DiscrTree Lean.Meta.Simp.SimprocEntry

structure Lean.Meta.Simp.Simprocs : Type

• pre : SimprocTree
• post : SimprocTree
• simprocNames : PHashSet Name
• erased : PHashSet Name

Instances For

• Lean.Meta.Simp.instInhabitedSimprocs

instance Lean.Meta.Simp.instInhabitedSimprocs : Inhabited Simprocs

Equations

• Lean.Meta.Simp.instInhabitedSimprocs = { default := { pre := default, post := default, simprocNames := default, erased := default } }

structure Lean.Meta.Simp.Methods : Type

• pre : Simproc
• post : Simproc
• dpre : DSimproc
• dpost : DSimproc
• discharge? : Expr → SimpM (Option Expr)
• wellBehavedDischarge : Bool

  wellBehavedDischarge must not be set to true IF discharge? access local declarations with index >= Context.lctxInitIndices when contextual := false. Reason: it would prevent us from aggressively caching simp results.

Instances For

• Lean.Meta.Simp.instInhabitedMethods

instance Lean.Meta.Simp.instInhabitedMethods : Inhabited Methods

Equations

• Lean.Meta.Simp.instInhabitedMethods = { default := { pre := default, post := default, dpre := default, dpost := default, discharge? := default, wellBehavedDischarge := default } }

unsafe def Lean.Meta.Simp.Methods.toMethodsRefImpl (m : Methods) : Lean.Meta.Simp.MethodsRef✝

Equations

• m.toMethodsRefImpl = unsafeCast m

@[implemented_by Lean.Meta.Simp.Methods.toMethodsRefImpl]

opaque Lean.Meta.Simp.Methods.toMethodsRef (m : Methods) : Lean.Meta.Simp.MethodsRef✝

unsafe def Lean.Meta.Simp.MethodsRef.toMethodsImpl (m : Lean.Meta.Simp.MethodsRef✝) : Methods

Equations

• Lean.Meta.Simp.MethodsRef.toMethodsImpl m = unsafeCast m

@[implemented_by Lean.Meta.Simp.MethodsRef.toMethodsImpl]

opaque Lean.Meta.Simp.MethodsRef.toMethods (m : Lean.Meta.Simp.MethodsRef✝) : Methods

def Lean.Meta.Simp.getMethods : SimpM Methods

Equations

• Lean.Meta.Simp.getMethods = do let __do_lift ← read pure (Lean.Meta.Simp.MethodsRef.toMethods __do_lift)

def Lean.Meta.Simp.pre (e : Expr) : SimpM Step

Equations

• Lean.Meta.Simp.pre e = do let __do_lift ← Lean.Meta.Simp.getMethods __do_lift.pre e

def Lean.Meta.Simp.post (e : Expr) : SimpM Step

Equations

• Lean.Meta.Simp.post e = do let __do_lift ← Lean.Meta.Simp.getMethods __do_lift.post e

@[inline]

def Lean.Meta.Simp.getContext : SimpM Context

Equations

• Lean.Meta.Simp.getContext = readThe Lean.Meta.Simp.Context

def Lean.Meta.Simp.getConfig : SimpM Config

Equations

• Lean.Meta.Simp.getConfig = do let __do_lift ← Lean.Meta.Simp.getContext pure __do_lift.config

@[inline]

def Lean.Meta.Simp.withParent {α : Type} (parent : Expr) (f : SimpM α) : SimpM α

Equations

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

def Lean.Meta.Simp.getSimpTheorems : SimpM SimpTheoremsArray

Equations

• Lean.Meta.Simp.getSimpTheorems = do let __do_lift ← readThe Lean.Meta.Simp.Context pure __do_lift.simpTheorems

def Lean.Meta.Simp.getSimpCongrTheorems : SimpM SimpCongrTheorems

Equations

• Lean.Meta.Simp.getSimpCongrTheorems = do let __do_lift ← readThe Lean.Meta.Simp.Context pure __do_lift.congrTheorems

def Lean.Meta.Simp.inDSimp : SimpM Bool

Returns true if simp is in dsimp mode. That is, only transformations that preserve definitional equality should be applied.

Equations

• Lean.Meta.Simp.inDSimp = do let __do_lift ← readThe Lean.Meta.Simp.Context pure __do_lift.inDSimp

@[inline]

def Lean.Meta.Simp.withPreservedCache {α : Type} (x : SimpM α) : SimpM α

Equations

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

@[inline]

def Lean.Meta.Simp.withFreshCache {α : Type} (x : SimpM α) : SimpM α

Save current cache, reset it, execute x, and then restore original cache.

Equations

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

@[inline]

def Lean.Meta.Simp.withDischarger {α : Type} (discharge? : Expr → SimpM (Option Expr)) (wellBehavedDischarge : Bool) (x : SimpM α) : SimpM α

Equations

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

def Lean.Meta.Simp.recordTriedSimpTheorem (thmId : Origin) : SimpM Unit

Equations

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

def Lean.Meta.Simp.recordSimpTheorem (thmId : Origin) : SimpM Unit

Equations

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

def Lean.Meta.Simp.recordCongrTheorem (declName : Name) : SimpM Unit

Equations

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

def Lean.Meta.Simp.recordTheoremWithBadKeys (thm : SimpTheorem) : SimpM Unit

Equations

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

def Lean.Meta.Simp.Result.getProof (r : Result) : MetaM Expr

Equations

• r.getProof = match r.proof? with | some p => pure p | none => Lean.Meta.mkEqRefl r.expr

def Lean.Meta.Simp.Result.getProof' (source : Expr) (r : Result) : MetaM Expr

Similar to Result.getProof, but adds a mkExpectedTypeHint if proof? is none (i.e., result is definitionally equal to input), but we cannot establish that source and r.expr are definitionally when using TransparencyMode.reducible.

Equations

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

def Lean.Meta.Simp.Result.mkCast (r : Result) (e : Expr) : MetaM Expr

Construct the Expr cast h e, from a Simp.Result with proof h.

Equations

• r.mkCast e = do let __do_lift ← r.getProof Lean.Meta.mkAppM `cast #[__do_lift, e]

def Lean.Meta.Simp.mkCongrFun (r : Result) (a : Expr) : MetaM Result

Equations

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

def Lean.Meta.Simp.mkCongr (r₁ r₂ : Result) : MetaM Result

Equations

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

def Lean.Meta.Simp.mkImpCongr (src : Expr) (r₁ r₂ : Result) : MetaM Result

Equations

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

def Lean.Meta.Simp.removeUnnecessaryCasts (e : Expr) : MetaM Expr

Given the application e, remove unnecessary casts of the form Eq.rec a rfl and Eq.ndrec a rfl.

Equations

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

def Lean.Meta.Simp.removeUnnecessaryCasts.isDummyEqRec (e : Expr) : Bool

Equations

• Lean.Meta.Simp.removeUnnecessaryCasts.isDummyEqRec e = ((e.isAppOfArity `Eq.rec 6 || e.isAppOfArity `Eq.ndrec 6) && e.appArg!.isAppOf `Eq.refl)

partial def Lean.Meta.Simp.removeUnnecessaryCasts.elimDummyEqRec (e : Expr) : Expr

def Lean.Meta.Simp.congrArgs (r : Result) (args : Array Expr) : SimpM Result

Given a simplified function result r and arguments args, simplify arguments using simp and dsimp. The resulting proof is built using congr and congrFun theorems.

Equations

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

def Lean.Meta.Simp.mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem)

Retrieve auto-generated congruence lemma for f.

Remark: If all argument kinds are fixed or eq, it returns none because using simple congruence theorems congr, congrArg, and congrFun produces a more compact proof.

Equations

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

def Lean.Meta.Simp.tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result)

Try to use automatically generated congruence theorems. See mkCongrSimp?.

Equations

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

def Lean.Meta.Simp.Result.addExtraArgs (r : Result) (extraArgs : Array Expr) : MetaM Result

Equations

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

def Lean.Meta.Simp.Step.addExtraArgs (s : Step) (extraArgs : Array Expr) : MetaM Step

Equations

• (Lean.Meta.Simp.Step.visit r).addExtraArgs extraArgs = do let __do_lift ← r.addExtraArgs extraArgs pure (Lean.Meta.Simp.Step.visit __do_lift)
• (Lean.Meta.Simp.Step.done r).addExtraArgs extraArgs = do let __do_lift ← r.addExtraArgs extraArgs pure (Lean.Meta.Simp.Step.done __do_lift)
• Lean.Meta.Simp.Step.continue.addExtraArgs extraArgs = pure Lean.Meta.Simp.Step.continue
• (Lean.Meta.Simp.Step.continue (some r)).addExtraArgs extraArgs = do let __do_lift ← r.addExtraArgs extraArgs pure (Lean.Meta.Simp.Step.continue (some __do_lift))

def Lean.Meta.Simp.DStep.addExtraArgs (s : DStep) (extraArgs : Array Expr) : DStep

Equations

• Lean.Meta.Simp.DStep.addExtraArgs (Lean.TransformStep.visit eNew) extraArgs = Lean.TransformStep.visit (Lean.mkAppN eNew extraArgs)
• Lean.Meta.Simp.DStep.addExtraArgs (Lean.TransformStep.done eNew) extraArgs = Lean.TransformStep.done (Lean.mkAppN eNew extraArgs)
• Lean.Meta.Simp.DStep.addExtraArgs Lean.TransformStep.continue extraArgs = Lean.TransformStep.continue
• Lean.Meta.Simp.DStep.addExtraArgs (Lean.TransformStep.continue (some eNew)) extraArgs = Lean.TransformStep.continue (some (Lean.mkAppN eNew extraArgs))

def Lean.Meta.applySimpResultToTarget (mvarId : MVarId) (target : Expr) (r : Simp.Result) : MetaM MVarId

Auxiliary method. Given the current target of mvarId, apply r which is a new target and proof that it is equal to the current one.

Equations

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