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: Dec 20 2023 at 11:08 UTC