-
Notifications
You must be signed in to change notification settings - Fork 39
Issues
is:issue state:open
is:issue state:open
Issue creation is restricted in this repository
Search results
- Status: Open.#480 In leanprover-community/iris-lean;
simpcan exit the ProofModebugSomething isn't workingSomething isn't workingStatus: Open.#469 In leanprover-community/iris-lean;- Status: Open.#468 In leanprover-community/iris-lean;
- Status: 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;Port iris_heap_lang/proofmode.v
featNew feature or requestNew feature or requestportingPorting Rocq developmentPorting Rocq developmentproof-modeProofMode porting tasksProofMode porting tasksStatus: Open.#431 In leanprover-community/iris-lean;Completeness
experimentIdeas for features that may or may not workIdeas for features that may or may not workfeatNew feature or requestNew feature or requestStatus: Open.#429 In leanprover-community/iris-lean;Guarded fixpoints
experimentIdeas for features that may or may not workIdeas for features that may or may not workfeatNew feature or requestNew feature or requestStatus: Open.#428 In leanprover-community/iris-lean;Iris data structures
experimentIdeas for features that may or may not workIdeas for features that may or may not workfeatNew feature or requestNew feature or requestStatus: Open.#427 In leanprover-community/iris-lean;