-
Notifications
You must be signed in to change notification settings - Fork 62
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Remove custom Instance of Countable
ImprovementNot a bug, but something can still be improvedNot a bug, but something can still be improvedStatus: Open.#669 In leanprover-community/iris-lean;Explore alternatives to typeclass inference to specify inclusion in GF
ImprovementNot a bug, but something can still be improvedNot a bug, but something can still be improvedStatus: Open.#654 In leanprover-community/iris-lean;- Status: Open.#623 In leanprover-community/iris-lean;
doc: Add a
rocq_ignorevariant for asserting that a typeclass instance existsImprovementNot a bug, but something can still be improvedNot a bug, but something can still be improvedStatus: Open.#615 In leanprover-community/iris-lean;- Status: Open.#603 In leanprover-community/iris-lean;
doc: Codify a consistent set of rules for
#rocq_ignoreandrocq_aliasdocumentationImprovements or additions to documentationImprovements or additions to documentationStatus: Open.#581 In leanprover-community/iris-lean;linter.checkUnivs triggers for
BundledGFunctorsand other definitions.ImprovementNot a bug, but something can still be improvedNot a bug, but something can still be improvedStatus: Open.#517 In leanprover-community/iris-lean;Debug mode for tactics
experimentIdeas for features that may or may not workIdeas for features that may or may not workImprovementNot a bug, but something can still be improvedNot a bug, but something can still be improvedquestionFurther information is requestedFurther information is requestedStatus: Open.#459 In leanprover-community/iris-lean;Experiment: Qp to Rat
experimentIdeas for features that may or may not workIdeas for features that may or may not workStatus: Open.#453 In leanprover-community/iris-lean;iframe alterations
proof-modeProofMode porting tasksProofMode porting tasksStatus: Open.#438 In leanprover-community/iris-lean;Investigate constructions fixed at
TypebugSomething isn't workingSomething isn't workingStatus: Open.#436 In leanprover-community/iris-lean;Port iris_heap_lang/class_instances.v and iris_heap_lang/primitive_laws.v
featNew feature or requestNew feature or requestportingPorting Rocq developmentPorting Rocq developmentStatus: Open.#432 In leanprover-community/iris-lean;