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: Jun 24 2024 at 01:01 UTC