- Sep 11, 2024
- Sep 10, 2024
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Sep 05, 2024
-
-
Robbert Krebbers authored
-
- Sep 04, 2024
-
-
Ralf Jung authored
Reformat style guide See merge request iris/iris!1072
-
Ralf Jung authored
-
Ralf Jung authored
Add some helpers for `discrete_fun_singleton` See merge request iris/iris!1071
-
Ralf Jung authored
-
- Sep 03, 2024
-
-
Janggun Lee authored
-
Robbert Krebbers authored
-
- Aug 30, 2024
-
-
Ralf Jung authored
-
- Aug 29, 2024
-
-
Janggun Lee authored
-
Ralf Jung authored
Add `discrete_fun_update{P}`. See merge request iris/iris!1070 -
Janggun Lee authored
-
- Aug 28, 2024
-
-
Ralf Jung authored
-
Janggun Lee authored
-
- Aug 23, 2024
-
-
Janggun Lee authored
* `updateP` requires `Finite A`, similar to `discrete_fun_included_spec`. * `update` has no such side conditions.
-
- Aug 20, 2024
-
-
Robbert Krebbers authored
iFrame: Do not call `cbv` on user terms in contexts See merge request iris/iris!1042
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Jan-Oliver Kaiser authored
-
- Aug 19, 2024
-
-
Ralf Jung authored
Use IH names from Coq intro pattern in `iInduction`. Closes #574 See merge request iris/iris!1063
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Add `iUnfold` tactic. Closes #573 See merge request iris/iris!1066
-
- Aug 17, 2024
-
-
Ralf Jung authored
Add instances for `match` on `Persistent`, `Affine`, `Absorbing`, `Plain`, `Timeless` Closes #479 See merge request iris/iris!1068
-
- Aug 16, 2024
-
-
Sanjit Bhat authored -
Sanjit Bhat authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Use `#[local] field ::` to make `inG` instances local. Closes #561 See merge request iris/iris!1065
-
