-
Notifications
You must be signed in to change notification settings - Fork 55
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Stale porting entries against Iris Rocq master
stale-portingStale rocq_alias or rocq_ignoreStale rocq_alias or rocq_ignoreStatus: Open.#593 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;- Status: Open.#562 In leanprover-community/iris-lean;
Recursion limit reached for invariants with names of more than 2 letters
bugSomething isn't workingSomething isn't workingStatus: Open.#557 In leanprover-community/iris-lean;Go-to-definition broken under
ipropnotationbugSomething isn't workingSomething isn't workingStatus: Open.#535 In leanprover-community/iris-lean;Derived laws: arrays
claimedSomebody is working on thisSomebody is working on thisfeatNew feature or requestNew feature or requestportingPorting Rocq developmentPorting Rocq developmentStatus: Open.#526 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;Port HeapLang tactics
claimedSomebody is working on thisSomebody is working on thisportingPorting Rocq developmentPorting Rocq developmentproof-modeProofMode porting tasksProofMode porting tasksStatus: Open.#480 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;