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

@[implicit_reducible, always_inline]

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

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

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

@[implicit_reducible]

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

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

@[reducible, inline]

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

Helper function for lifting a AlphaShareBuilderM action to GrindM

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

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

@[implicit_reducible]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

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

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

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

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

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

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

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

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

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

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

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.

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.

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.

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.