Helper functions for constructing maximally shared expressions from maximally shared expressions. That is, mkAppS f a assumes that f and a are maximally shared.

These functions are in the Internal namespace because they can be easily misused. We use them to construct safe functions.

class Lean.Meta.Sym.Internal.MonadShareCommon (m : Type → Type) : Type

• share1 : Expr → m Expr
• assertShared : Expr → m Unit
• isDebugEnabled : m Bool

@[instance_reducible, always_inline]

instance Lean.Meta.Sym.Internal.instMonadShareCommonOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadShareCommon m] : MonadShareCommon n

Equations

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

def Lean.Meta.Sym.Internal.Sym.share1 (e : Expr) : SymM Expr

Equations

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

def Lean.Meta.Sym.Internal.Sym.assertShared (e : Expr) : SymM Unit

Equations

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

@[instance_reducible]

instance Lean.Meta.Sym.Internal.instMonadShareCommonSymM : MonadShareCommon SymM

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Sym.Internal.AlphaShareBuilderM (α : Type) : Type

Helper monad for constructing maximally shared terms. The Bool flag indicates whether it is debug-mode or not.

Equations

• Lean.Meta.Sym.Internal.AlphaShareBuilderM = ReaderT Bool Lean.Meta.Sym.AlphaShareCommonM

@[reducible, inline]

abbrev Lean.Meta.Sym.Internal.liftBuilderM {α : Type} (k : AlphaShareBuilderM α) : SymM α

Helper function for lifting a AlphaShareBuilderM action to GrindM

Equations

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

def Lean.Meta.Sym.Internal.Builder.share1 (e : Expr) : AlphaShareBuilderM Expr

Equations

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

def Lean.Meta.Sym.Internal.Builder.assertShared (e : Expr) : AlphaShareBuilderM Unit

Equations

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

@[instance_reducible]

instance Lean.Meta.Sym.Internal.instMonadShareCommonAlphaShareBuilderM : MonadShareCommon AlphaShareBuilderM

Equations

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

def Lean.Meta.Sym.Internal.mkLitS {m : Type → Type} [MonadShareCommon m] (l : Literal) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkLitS l = Lean.Meta.Sym.Internal.MonadShareCommon.share1 (Lean.Expr.lit l)

def Lean.Meta.Sym.Internal.mkConstS {m : Type → Type} [MonadShareCommon m] (declName : Name) (us : List Level := []) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkConstS declName us = Lean.Meta.Sym.Internal.MonadShareCommon.share1 (Lean.Expr.const declName us)

def Lean.Meta.Sym.Internal.mkBVarS {m : Type → Type} [MonadShareCommon m] (idx : Nat) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkBVarS idx = Lean.Meta.Sym.Internal.MonadShareCommon.share1 (Lean.Expr.bvar idx)

def Lean.Meta.Sym.Internal.mkSortS {m : Type → Type} [MonadShareCommon m] (u : Level) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkSortS u = Lean.Meta.Sym.Internal.MonadShareCommon.share1 (Lean.Expr.sort u)

def Lean.Meta.Sym.Internal.mkFVarS {m : Type → Type} [MonadShareCommon m] (fvarId : FVarId) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkFVarS fvarId = Lean.Meta.Sym.Internal.MonadShareCommon.share1 (Lean.Expr.fvar fvarId)

def Lean.Meta.Sym.Internal.mkMVarS {m : Type → Type} [MonadShareCommon m] (mvarId : MVarId) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkMVarS mvarId = Lean.Meta.Sym.Internal.MonadShareCommon.share1 (Lean.Expr.mvar mvarId)

def Lean.Meta.Sym.Internal.mkMDataS {m : Type → Type} [MonadShareCommon m] [Monad m] (d : MData) (e : Expr) : m Expr

Equations

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

def Lean.Meta.Sym.Internal.mkProjS {m : Type → Type} [MonadShareCommon m] [Monad m] (structName : Name) (idx : Nat) (struct : Expr) : m Expr

Equations

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

def Lean.Meta.Sym.Internal.mkAppS {m : Type → Type} [MonadShareCommon m] [Monad m] (f a : Expr) : m Expr

Equations

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

def Lean.Meta.Sym.Internal.mkLambdaS {m : Type → Type} [MonadShareCommon m] [Monad m] (x : Name) (bi : BinderInfo) (t b : Expr) : m Expr

Equations

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

def Lean.Meta.Sym.Internal.mkForallS {m : Type → Type} [MonadShareCommon m] [Monad m] (x : Name) (bi : BinderInfo) (t b : Expr) : m Expr

Equations

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

def Lean.Meta.Sym.Internal.mkLetS {m : Type → Type} [MonadShareCommon m] [Monad m] (x : Name) (t v b : Expr) (nondep : Bool := false) : m Expr

Equations

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

def Lean.Meta.Sym.Internal.mkHaveS {m : Type → Type} [MonadShareCommon m] [Monad m] (x : Name) (t v b : Expr) : m Expr

Equations

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

@[inline]

def Lean.Expr.updateAppS! {m : Type → Type} [Meta.Sym.Internal.MonadShareCommon m] [Monad m] (e newFn newArg : Expr) : m Expr

Equations

• (fn.app arg).updateAppS! newFn newArg = if (Lean.Meta.Sym.isSameExpr fn newFn && Lean.Meta.Sym.isSameExpr arg newArg) = true then pure (fn.app arg) else Lean.Meta.Sym.Internal.mkAppS newFn newArg
• e.updateAppS! newFn newArg = panicWithPosWithDecl "Lean.Meta.Sym.AlphaShareBuilder" "Lean.Expr.updateAppS!" 148 25 "application expected"

@[inline]

def Lean.Expr.updateMDataS! {m : Type → Type} [Meta.Sym.Internal.MonadShareCommon m] [Monad m] (e newExpr : Expr) : m Expr

Equations

• (Lean.Expr.mdata d a).updateMDataS! newExpr = if Lean.Meta.Sym.isSameExpr a newExpr = true then pure (Lean.Expr.mdata d a) else Lean.Meta.Sym.Internal.mkMDataS d newExpr
• e.updateMDataS! newExpr = panicWithPosWithDecl "Lean.Meta.Sym.AlphaShareBuilder" "Lean.Expr.updateMDataS!" 152 24 "mdata expected"

@[inline]

def Lean.Expr.updateProjS! {m : Type → Type} [Meta.Sym.Internal.MonadShareCommon m] [Monad m] (e newExpr : Expr) : m Expr

Equations

• (Lean.Expr.proj s i a).updateProjS! newExpr = if Lean.Meta.Sym.isSameExpr a newExpr = true then pure (Lean.Expr.proj s i a) else Lean.Meta.Sym.Internal.mkProjS s i newExpr
• e.updateProjS! newExpr = panicWithPosWithDecl "Lean.Meta.Sym.AlphaShareBuilder" "Lean.Expr.updateProjS!" 156 25 "proj expected"

@[inline]

def Lean.Expr.updateForallS! {m : Type → Type} [Meta.Sym.Internal.MonadShareCommon m] [Monad m] (e newDomain newBody : Expr) : m Expr

Equations

• One or more equations did not get rendered due to their size.
• e.updateForallS! newDomain newBody = panicWithPosWithDecl "Lean.Meta.Sym.AlphaShareBuilder" "Lean.Expr.updateForallS!" 160 31 "forall expected"

@[inline]

def Lean.Expr.updateLambdaS! {m : Type → Type} [Meta.Sym.Internal.MonadShareCommon m] [Monad m] (e newDomain newBody : Expr) : m Expr

Equations

• One or more equations did not get rendered due to their size.
• e.updateLambdaS! newDomain newBody = panicWithPosWithDecl "Lean.Meta.Sym.AlphaShareBuilder" "Lean.Expr.updateLambdaS!" 167 27 "lambda expected"

@[inline]

def Lean.Expr.updateLetS! {m : Type → Type} [Meta.Sym.Internal.MonadShareCommon m] [Monad m] (e newType newVal newBody : Expr) : m Expr

Equations

• One or more equations did not get rendered due to their size.
• e.updateLetS! newType newVal newBody = panicWithPosWithDecl "Lean.Meta.Sym.AlphaShareBuilder" "Lean.Expr.updateLetS!" 174 34 "let expression expected"

def Lean.Meta.Sym.Internal.mkAppS₂ {m : Type → Type} [MonadShareCommon m] [Monad m] (f a₁ a₂ : Expr) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkAppS₂ f a₁ a₂ = do let __do_lift ← Lean.Meta.Sym.Internal.mkAppS f a₁ Lean.Meta.Sym.Internal.mkAppS __do_lift a₂

def Lean.Meta.Sym.Internal.mkAppS₃ {m : Type → Type} [MonadShareCommon m] [Monad m] (f a₁ a₂ a₃ : Expr) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkAppS₃ f a₁ a₂ a₃ = do let __do_lift ← Lean.Meta.Sym.Internal.mkAppS₂ f a₁ a₂ Lean.Meta.Sym.Internal.mkAppS __do_lift a₃

def Lean.Meta.Sym.Internal.mkAppS₄ {m : Type → Type} [MonadShareCommon m] [Monad m] (f a₁ a₂ a₃ a₄ : Expr) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkAppS₄ f a₁ a₂ a₃ a₄ = do let __do_lift ← Lean.Meta.Sym.Internal.mkAppS₃ f a₁ a₂ a₃ Lean.Meta.Sym.Internal.mkAppS __do_lift a₄

def Lean.Meta.Sym.Internal.mkAppS₅ {m : Type → Type} [MonadShareCommon m] [Monad m] (f a₁ a₂ a₃ a₄ a₅ : Expr) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkAppS₅ f a₁ a₂ a₃ a₄ a₅ = do let __do_lift ← Lean.Meta.Sym.Internal.mkAppS₄ f a₁ a₂ a₃ a₄ Lean.Meta.Sym.Internal.mkAppS __do_lift a₅

def Lean.Meta.Sym.Internal.mkAppS₆ {m : Type → Type} [MonadShareCommon m] [Monad m] (f a₁ a₂ a₃ a₄ a₅ a₆ : Expr) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkAppS₆ f a₁ a₂ a₃ a₄ a₅ a₆ = do let __do_lift ← Lean.Meta.Sym.Internal.mkAppS₅ f a₁ a₂ a₃ a₄ a₅ Lean.Meta.Sym.Internal.mkAppS __do_lift a₆

def Lean.Meta.Sym.Internal.mkAppS₇ {m : Type → Type} [MonadShareCommon m] [Monad m] (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ : Expr) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkAppS₇ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ = do let __do_lift ← Lean.Meta.Sym.Internal.mkAppS₆ f a₁ a₂ a₃ a₄ a₅ a₆ Lean.Meta.Sym.Internal.mkAppS __do_lift a₇

def Lean.Meta.Sym.Internal.mkAppS₈ {m : Type → Type} [MonadShareCommon m] [Monad m] (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : Expr) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkAppS₈ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ = do let __do_lift ← Lean.Meta.Sym.Internal.mkAppS₇ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ Lean.Meta.Sym.Internal.mkAppS __do_lift a₈

def Lean.Meta.Sym.Internal.mkAppS₉ {m : Type → Type} [MonadShareCommon m] [Monad m] (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ : Expr) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkAppS₉ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ = do let __do_lift ← Lean.Meta.Sym.Internal.mkAppS₈ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ Lean.Meta.Sym.Internal.mkAppS __do_lift a₉

def Lean.Meta.Sym.Internal.mkAppS₁₀ {m : Type → Type} [MonadShareCommon m] [Monad m] (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ : Expr) : m Expr

Equations

• Lean.Meta.Sym.Internal.mkAppS₁₀ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ = do let __do_lift ← Lean.Meta.Sym.Internal.mkAppS₉ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Lean.Meta.Sym.Internal.mkAppS __do_lift a₁₀

def Lean.Meta.Sym.Internal.mkAppS₁₁ {m : Type → Type} [MonadShareCommon m] [Monad m] (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ a₁₁ : Expr) : m Expr

Equations

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

def Lean.Meta.Sym.Internal.mkAppRangeS {m : Type → Type} [MonadShareCommon m] [Monad m] (f : Expr) (beginIdx endIdx : Nat) (args : Array Expr) : m Expr

mkAppRangeS f i j #[a₀, ..., aᵢ, ..., aⱼ, ...] ==> f aᵢ ... aⱼ₋₁ with max sharing.

Equations

• Lean.Meta.Sym.Internal.mkAppRangeS f beginIdx endIdx args = Lean.Meta.Sym.Internal.mkAppRangeS.go✝ args endIdx f beginIdx

def Lean.Meta.Sym.Internal.mkAppNS {m : Type → Type} [MonadShareCommon m] [Monad m] (f : Expr) (args : Array Expr) : m Expr

mkAppNS f #[a₀, ..., aₙ] constructs f a₀ ... aₙ with max sharing.

Equations

• Lean.Meta.Sym.Internal.mkAppNS f args = Lean.Meta.Sym.Internal.mkAppRangeS f 0 args.size args

def Lean.Meta.Sym.Internal.mkAppRevRangeS {m : Type → Type} [MonadShareCommon m] [Monad m] (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : m Expr

mkAppRevRangeS f b e revArgs ==> mkAppRev f (revArgs.extract b e) with max sharing.

Equations

• Lean.Meta.Sym.Internal.mkAppRevRangeS f beginIdx endIdx revArgs = Lean.Meta.Sym.Internal.mkAppRevRangeS.go✝ revArgs beginIdx f endIdx

def Lean.Meta.Sym.Internal.mkAppRevS {m : Type → Type} [MonadShareCommon m] [Monad m] (f : Expr) (revArgs : Array Expr) : m Expr

Same as mkAppS f args but reversing args, with max sharing.

Equations

• Lean.Meta.Sym.Internal.mkAppRevS f revArgs = Lean.Meta.Sym.Internal.mkAppRevRangeS f 0 revArgs.size revArgs