Issues · Iris · GitLab

weaker boolean?

refinedc#35 · created Apr 08, 2021 by Michael Sammler typesystem
- 0
updated Apr 08, 2021
Taking ∃ out of ▷ without Inhabited, more easily

iris#411 · created Mar 28, 2021 by Yusuke Matsushita A-coq C-enhancement T-proofmode
- 3
updated Mar 29, 2021
Modality for `Timeless`

iris#410 · created Mar 22, 2021 by Ralf Jung
- 1
- 2
updated Mar 22, 2021
Wrap notation in modules

stdpp#101 · created Mar 19, 2021 by Yishuai Li
- 2
updated Mar 19, 2021
Proposed change to naming convention for "dataful" `*G`s

iris#409 · created Mar 18, 2021 by Ralf Jung
- 3
updated Mar 23, 2021
bi.weakestpre imports a module from program_logic

iris#408 · created Mar 17, 2021 by Ralf Jung A-coq C-bug T-bi T-program_logic
- 2
- 7
updated Mar 18, 2021
Tracking issue for list RA

iris#407 · created Mar 17, 2021 by Ralf Jung C-tracking-issue T-algebra
- 0
updated Mar 17, 2021
set notation for multisets is broken: uses ∪ instead of ⊎

stdpp#100 · created Mar 10, 2021 by Robbert Krebbers
- 1
- 4
updated Mar 11, 2021
"(1 ≤ qmax)%Qp" simplifies to something horrible

stdpp#99 · created Mar 09, 2021 by Ralf Jung
- 2
updated Mar 09, 2021
Unexpected type cast generated by frontend

refinedc#34 · created Mar 04, 2021 by Fengmin Zhu bug frontend
- 0
updated Mar 04, 2021
Slow typechecking / nonterminating Qed when using auxiliary definitions in RAs

iris#406 · created Mar 03, 2021 by Armaël Guéneau A-coq C-bug I-performance T-algebra
- 3
updated Mar 18, 2021
elem_of_intersection not applicable to multisets

stdpp#98 · created Feb 17, 2021 by François Pottier
- 0
updated Feb 17, 2021
Tracking issue for HeapLang interpreter

iris#405 · created Feb 16, 2021 by Ralf Jung C-tracking-issue T-heap_lang
- 0
updated Feb 16, 2021
Nat.iter: theory for associative and commutative functions

stdpp#97 · created Feb 09, 2021 by Ralf Jung
- 0
updated Feb 09, 2021
iFrame performance issues

iris#402 · created Feb 03, 2021 by Ralf Jung A-coq C-enhancement I-performance T-proofmode
- 1
- 0
updated Feb 17, 2021
Find better place for pred_finite and pred_infinite

stdpp#96 · created Feb 01, 2021 by Ralf Jung
- 0
updated Feb 01, 2021
Integrate Tej's simp-lang?

iris#400 · created Jan 28, 2021 by Ralf Jung A-docs T-program_logic
- 5
updated Feb 17, 2021
Upstream more big_op lemmas from Perennial

iris#399 · created Jan 27, 2021 by Ralf Jung A-coq C-enhancement T-bi
- 1
updated Feb 17, 2021
Use `dom` instead of `∀ k, is_Some (.. !! k) ...`

iris#398 · created Jan 26, 2021 by Robbert Krebbers A-coq C-enhancement T-algebra T-bi
- 0
updated Feb 17, 2021
Hiding `spec_ctx`.

reloc#10 · created Jan 20, 2021 by Dan Frumin
- 0
updated Jan 20, 2021

Prev
1
2
3
4
5
…
11
Next