structure MaximizableProps : Type

def instToJsonMaximizableProps.toJson : MaximizableProps → Lean.Json

Equations

• instToJsonMaximizableProps.toJson x✝ = Lean.Json.mkObj [].flatten

@[instance_reducible]

instance instToJsonMaximizableProps : Lean.ToJson MaximizableProps

Equations

• instToJsonMaximizableProps = { toJson := instToJsonMaximizableProps.toJson }

def instFromJsonMaximizableProps.fromJson : Lean.Json → Except String MaximizableProps

Equations

• instFromJsonMaximizableProps.fromJson json✝ = pure { }

@[instance_reducible]

instance instFromJsonMaximizableProps : Lean.FromJson MaximizableProps

Equations

• instFromJsonMaximizableProps = { fromJson? := instFromJsonMaximizableProps.fromJson }

def Maximizable : ProofWidgets.Component MaximizableProps

Wraps its children in a <div> that can be maximized to take up the whole viewport by clicking a button in the top-right corner.

Equations

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