def ProofWidgets.Util.joinArrays {m : Type → Type} [Monad m] [Lean.MonadRef m] [Lean.MonadQuotation m] (arr : Array Lean.Term) : m Lean.Term

Sends #[a, b, c] to `(term| $a ++ $b ++ $c)

Equations

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

def ProofWidgets.Util.foldInlsM {α β : Type u_1} {m : Type u_1 → Type u_2} [Monad m] (arr : Array (α ⊕ β)) (f : Array α → m β) : m (Array β)

Collapse adjacent inl (_ : α)s into a β using f. For example, #[.inl a₁, .inl a₂, .inr b, .inl a₃] ↦ #[← f #[a₁, a₂], b, ← f #[a₃]].

Equations

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

def Lean.PrettyPrinter.Delaborator.delabListLiteral {α : Type} (elem : DelabM α) : DelabM (Array α)

Delaborate the elements of a list literal separately, calling elem on each.

Equations

• Lean.PrettyPrinter.Delaborator.delabListLiteral elem = Lean.PrettyPrinter.Delaborator.delabListLiteral.go✝ elem #[]

def Lean.PrettyPrinter.Delaborator.delabArrayLiteral {α : Type} (elem : DelabM α) : DelabM (Array α)

Delaborate the elements of an array literal separately, calling elem on each.

Equations

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

def Lean.PrettyPrinter.Delaborator.annotateTermLikeInfo {n : SyntaxNodeKinds} (stx : TSyntax n) : DelabM (TSyntax n)

A copy of Delaborator.annotateTermInfo for other syntactic categories.

Equations

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

def Lean.PrettyPrinter.Delaborator.withAnnotateTermLikeInfo {n : SyntaxNodeKinds} (d : DelabM (TSyntax n)) : DelabM (TSyntax n)

A copy of Delaborator.withAnnotateTermInfo for other syntactic categories.

Equations

• Lean.PrettyPrinter.Delaborator.withAnnotateTermLikeInfo d = do let stx ← d Lean.PrettyPrinter.Delaborator.annotateTermLikeInfo stx

class MonadSaveCtx (m : Type → Type) (n : outParam (Type → Type)) : Type 1

Certain monad transformers such as ReaderT and StateT/StateRefT provide additional context (read-only) and state (mutable). MonadSaveCtx m n means that m is a stack of contexts/states on top of n. It provides a way to suspend an m-action by saving the "current" value of this stack.

For example, m = Lean.MetaM is a stack of contexts and states on top of n = EIO Lean.Exception. Thus we have saveCtxM : Lean.MetaM α → Lean.MetaM (EIO Lean.Exception α).

• saveCtxM {α : Type} : m α → m (n α)

  Transform an action x : m α into an action m (n α) that

  • saves the current context/state of m; and
  • returns an action y : n α that would use the saved context/state if run. Note that because y no longer has access to m's state, any StateT changes that it makes when you run it later will be discarded.

@[implicit_reducible]

instance instMonadSaveCtx {m : Type → Type} [Monad m] : MonadSaveCtx m m

Equations

• instMonadSaveCtx = { saveCtxM := fun {α : Type} => pure }

@[implicit_reducible]

instance instMonadSaveCtxReaderT {m n : Type → Type} [MonadSaveCtx m n] {ρ : Type} : MonadSaveCtx (ReaderT ρ m) n

Equations

• instMonadSaveCtxReaderT = { saveCtxM := fun {α : Type} (act : ReaderT ρ m α) (ctx : ρ) => saveCtxM (act ctx) }

@[implicit_reducible]

instance instMonadSaveCtxStateT {m n : Type → Type} [Monad m] [MonadSaveCtx m n] {σ : Type} : MonadSaveCtx (StateT σ m) n

Equations

• instMonadSaveCtxStateT = { saveCtxM := fun {α : Type} (act : StateT σ m α) => do let __do_lift ← get liftM (saveCtxM (act.run' __do_lift)) }

@[implicit_reducible]

instance instMonadSaveCtxStateRefT'OfMonadLiftTST {m n : Type → Type} [Monad m] [MonadSaveCtx m n] {ω σ : Type} [MonadLiftT (ST ω) m] : MonadSaveCtx (StateRefT' ω σ m) n

Equations

• instMonadSaveCtxStateRefT'OfMonadLiftTST = { saveCtxM := fun {α : Type} (act : StateRefT' ω σ m α) => do let __do_lift ← get liftM (saveCtxM (act.run' __do_lift)) }

@[implicit_reducible]

instance instToJsonUnit_proofWidgets : Lean.ToJson Unit

Equations

• instToJsonUnit_proofWidgets = { toJson := fun (x : Unit) => Lean.Json.null }

@[implicit_reducible]

instance instFromJsonUnit_proofWidgets : Lean.FromJson Unit

Equations

• instFromJsonUnit_proofWidgets = { fromJson? := fun (x : Lean.Json) => Except.ok () }