Zulip Chat Archive
Stream: new members
Topic: Local instance
Joachim Breitner (Jan 13 2022 at 15:38):
After something like
have Hfin : fintype (generators H) := …,
how do I make that local fact available to the instance resolution afterwards?
Yaël Dillies (Jan 13 2022 at 15:38):
Use haveI instead of have.
Yaël Dillies (Jan 13 2022 at 15:39):
Similarly, you have exactI and applyI
Last updated: May 02 2025 at 03:31 UTC