Stream: Coq users

Topic: Change plicity of context in section?

Shea Levy (Oct 17 2020 at 22:46):

Is it possible to declare some variables in the context of a section as explicit, then later in the section make them implicit? Obviously I can just make a new section or call Arguments after the definition, just curious if there's a nicer way.

Last updated: Oct 13 2024 at 01:02 UTC