Extracting "properties" of the type

Stream: Is there code for X?

[Jan Idziak]

Newbie question about types.

In the NNG it is easy to understand how the MyNat type is constructed and what are the axioms (rules) that we can use.

Is a programmatic way with some kind of elaboration to extract the type information directly from lean.
Something like #typedefinitio MyNat to extract:

• constructor like inductive
• axioms like add_zero
• operators definitions: like +: N -> N -> N

Would appreciate any help or pointers on this topic!

[Jireh Loreaux]

You can use #whatsnew in before the type declaration to get the automatic stuff declared with the inductive type.

[Jireh Loreaux]

As for things declared on the type (like it's Add instance, you'll need to look it up manually to some extent. You can look at docs#Nat and then click on the "instances" arrow below it to see which instances are available.

[Jireh Loreaux]

You can also do #synth Add Nat

[Jireh Loreaux]

Note that Add is not part of the definition of the type Nat, which is the reason this has a separate procedure.