ad hoc types

Stream: new members

[King Arthur]

is it possible to define a whole new type of objects in the middle of a proof or does that necessarily have to be done outside? I want to define an inductive type and a function on that type for a proof, but I'm also curious if it's possible to do this for classes and structures

[Patrick Johnson]

Yes, it's possible using docs#W_type (see #leantt section 5).

[Patrick Johnson]

You can also do that for structures, but you won't get a nice syntax.