The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Apparently, it works to start a section and do "Local Arguments foo : 
clear implicit.".  Then, upon leaving the section, the implicits are 
returned.

That's acceptable, since in most cases, I don't need to parse foo when 
proving with foo...

-- Jonathan


On 06/24/2016 01:22 PM, Jonathan Leivent wrote:
> On 06/24/2016 01:08 PM, Ralf Jung wrote:
> > Hi,
> >
> > > Is there anything like an Arguments command that will allow only
> > > specifically chosen implicits to print?  I know I can do Arguments :
> > > clear implicits, but I don't want parsing impacted, and only 
> > > temporarily
> > > want printing impacted.  Set Printing Implicit is a blunt instrument.
> > > The Defensive modifier is also too blunt.  I'm hoping maybe there is an
> > > undocumented Argument command that already does this...
> > >
> > > The use case is: a particular function where the implicits work very
> > > well parsing-wise, but often become confusing during proving, as when
> > > one sees a conclusion like "foo x = foo x", but reflexivity fails 
> > > due to
> > > differences in the implicits (even f_equal fails to progress).  And
> > > there are many other implicits in other functions around working very
> > > nicely to make the goals easy to read, so using Set Printing Implicit,
> > > Defenisve or not, is not a good idea.  In such a case, it would be nice
> > > to do something like "Arguments foo : {no}print implicits" to turn them
> > > on and off, so that foo would always print as @foo.
> > One thing you could do is not have that argument implicit, and then
> > define a parsing only notation that adds the underscore to trigger
> > inference. Like
> >
> > Definition foo (n : nat) := n.
> > Notation foo' := (foo _) (only parsing).
> >
> > This means you have to use foo' when writing but will see foo in the
> > proof state; but other than that, I think the implicits should behave
> > the way you want.
> >
> > Kind regards,
> > Ralf
>
> I was thinking of something like that - actually was going to use 
> another function with implicits (foo') for parsing that just calls the 
> one without (foo) - then unfold foo' during proving would do the trick 
> - I could then even do it on a per hyp/occurrence basis - and then 
> re-fold if desired.  Would be even better if there was a variety of 
> transparency that auto-unfolded whenever needed (I think Jason logged 
> a request for something like that), so I wouldn't have to worry about 
> the impact the added layer of def has on the proof.
>
> But, I'm lazy, and this is really just a very minor annoyance. So, I 
> was wondering if the Arguments thing already existed...
>
> -- Jonathan