Stream: Coq users

Topic: Change plicity of context in section?


view this post on Zulip 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: Mar 29 2024 at 07:01 UTC