coq icon indicating copy to clipboard operation
coq copied to clipboard

Published 20 hours ago • verified publisher icon coq

Print Ltac2 Type

Open JasonGross opened this issue 3 years ago • 4 comments

I'd like to be able to write Print Ltac2 Type exn

JasonGross avatar Aug 28 '22 04:08 JasonGross

What does that mean?

SkySkimmer avatar Aug 29 '22 12:08 SkySkimmer

It should work like Print Ltac2, but print the type definition (i.e., print things defined via Ltac2 Type)

JasonGross avatar Aug 29 '22 16:08 JasonGross

So exn would show Ltac2 Type exn := [ .. ].?

SkySkimmer avatar Aug 29 '22 16:08 SkySkimmer

Yep, ideally with all the constructors that have been added to it, along with their types / what I'd have to type into Coq to get a copy of the type as it currently is

JasonGross avatar Aug 29 '22 17:08 JasonGross