5eef3d27fb
This PR improves the `#print` command for structures to show all fields
and which parents the fields were inherited from, hiding internal
details such as which parents are represented as subobjects. This
information is still present in the constructor if needed. The pretty
printer for private constants is also improved, and it now handles
private names from the current module like any other name; private names
from other modules are made hygienic.
Example output for `#print Monad`:
```
class Monad.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
number of parameters: 1
parents:
Monad.toApplicative : Applicative m
Monad.toBind : Bind m
fields:
Functor.map : {α β : Type u} → (α → β) → m α → m β
Functor.mapConst : {α β : Type u} → α → m β → m α
Pure.pure : {α : Type u} → α → m α
Seq.seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β
SeqLeft.seqLeft : {α β : Type u} → m α → (Unit → m β) → m α
SeqRight.seqRight : {α β : Type u} → m α → (Unit → m β) → m β
Bind.bind : {α β : Type u} → m α → (α → m β) → m β
constructor:
Monad.mk.{u, v} {m : Type u → Type v} [toApplicative : Applicative m] [toBind : Bind m] : Monad m
resolution order:
Monad, Applicative, Bind, Functor, Pure, Seq, SeqLeft, SeqRight
```
Suggested by Floris van Doorn [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.23print.20command.20for.20structures/near/482503637).
161 lines
4.3 KiB
Text
161 lines
4.3 KiB
Text
/-!
|
||
# Test `#print` command for structures and classes
|
||
-/
|
||
|
||
/-! Structure -/
|
||
/--
|
||
info: structure Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)
|
||
number of parameters: 2
|
||
fields:
|
||
Prod.fst : α
|
||
Prod.snd : β
|
||
constructor:
|
||
Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β
|
||
-/
|
||
#guard_msgs in
|
||
#print Prod
|
||
|
||
/-! Class -/
|
||
/--
|
||
info: class Inhabited.{u} (α : Sort u) : Sort (max 1 u)
|
||
number of parameters: 1
|
||
fields:
|
||
Inhabited.default : α
|
||
constructor:
|
||
Inhabited.mk.{u} {α : Sort u} (default : α) : Inhabited α
|
||
-/
|
||
#guard_msgs in
|
||
#print Inhabited
|
||
|
||
/-! Structure with private field, imported -/
|
||
/--
|
||
info: structure Thunk.{u} (α : Type u) : Type u
|
||
number of parameters: 1
|
||
fields:
|
||
private Thunk.fn✝ : Unit → α
|
||
constructor:
|
||
Thunk.mk.{u} {α : Type u} (fn : Unit → α) : Thunk α
|
||
-/
|
||
#guard_msgs in
|
||
#print Thunk
|
||
|
||
/-! Structure with private field, current module -/
|
||
structure PrivField where
|
||
private x : Nat
|
||
|
||
/--
|
||
info: structure PrivField : Type
|
||
number of parameters: 0
|
||
fields:
|
||
private PrivField.x : Nat
|
||
constructor:
|
||
PrivField.mk (x : Nat) : PrivField
|
||
-/
|
||
#guard_msgs in
|
||
#print PrivField
|
||
|
||
/-! Private constructor, imported -/
|
||
/--
|
||
info: class TypeName.{u} (α : Type u) : Type
|
||
number of parameters: 1
|
||
fields:
|
||
private TypeName.data✝ : (TypeNameData✝ α).type
|
||
constructor:
|
||
private TypeName.mk'✝.{u} {α : Type u} (data : (TypeNameData✝ α).type) : TypeName α
|
||
-/
|
||
#guard_msgs in
|
||
#print TypeName
|
||
|
||
/-! Private constructor, current module -/
|
||
structure PrivCtor where private mk ::
|
||
x : Nat
|
||
/--
|
||
info: structure PrivCtor : Type
|
||
number of parameters: 0
|
||
fields:
|
||
PrivCtor.x : Nat
|
||
constructor:
|
||
private PrivCtor.mk (x : Nat) : PrivCtor
|
||
-/
|
||
#guard_msgs in
|
||
#print PrivCtor
|
||
|
||
/-! Extended class -/
|
||
/--
|
||
info: class Alternative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
|
||
number of parameters: 1
|
||
parents:
|
||
Alternative.toApplicative : Applicative f
|
||
fields:
|
||
Functor.map : {α β : Type u} → (α → β) → f α → f β
|
||
Functor.mapConst : {α β : Type u} → α → f β → f α
|
||
Pure.pure : {α : Type u} → α → f α
|
||
Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
|
||
SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
|
||
SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β
|
||
Alternative.failure : {α : Type u} → f α
|
||
Alternative.orElse : {α : Type u} → f α → (Unit → f α) → f α
|
||
constructor:
|
||
Alternative.mk.{u, v} {f : Type u → Type v} [toApplicative : Applicative f] (failure : {α : Type u} → f α)
|
||
(orElse : {α : Type u} → f α → (Unit → f α) → f α) : Alternative f
|
||
resolution order:
|
||
Alternative, Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
|
||
-/
|
||
#guard_msgs in
|
||
#print Alternative
|
||
|
||
/-! Multiply extended class -/
|
||
/--
|
||
info: class Applicative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
|
||
number of parameters: 1
|
||
parents:
|
||
Applicative.toFunctor : Functor f
|
||
Applicative.toPure : Pure f
|
||
Applicative.toSeq : Seq f
|
||
Applicative.toSeqLeft : SeqLeft f
|
||
Applicative.toSeqRight : SeqRight f
|
||
fields:
|
||
Functor.map : {α β : Type u} → (α → β) → f α → f β
|
||
Functor.mapConst : {α β : Type u} → α → f β → f α
|
||
Pure.pure : {α : Type u} → α → f α
|
||
Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
|
||
SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
|
||
SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β
|
||
constructor:
|
||
Applicative.mk.{u, v} {f : Type u → Type v} [toFunctor : Functor f] [toPure : Pure f] [toSeq : Seq f]
|
||
[toSeqLeft : SeqLeft f] [toSeqRight : SeqRight f] : Applicative f
|
||
resolution order:
|
||
Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
|
||
-/
|
||
#guard_msgs in
|
||
#print Applicative
|
||
|
||
/-! Structure with unused parameter -/
|
||
|
||
structure Weird (α β : Type _) where
|
||
a : α
|
||
|
||
/--
|
||
info: structure Weird.{u_1, u_2} (α : Type u_1) (β : Type u_2) : Type u_1
|
||
number of parameters: 2
|
||
fields:
|
||
Weird.a : α
|
||
constructor:
|
||
Weird.mk.{u_1, u_2} {α : Type u_1} {β : Type u_2} (a : α) : Weird α β
|
||
-/
|
||
#guard_msgs in
|
||
#print Weird
|
||
|
||
/-! Structure-like inductive -/
|
||
|
||
inductive Fake (α : Type _) where
|
||
| mk : (x : α) → Fake α
|
||
|
||
/--
|
||
info: inductive Fake.{u_1} : Type u_1 → Type u_1
|
||
number of parameters: 1
|
||
constructors:
|
||
Fake.mk : {α : Type u_1} → α → Fake α
|
||
-/
|
||
#guard_msgs in
|
||
#print Fake
|