GenericMonkey

### Dafny version 4.9.1.0 ### Code to produce this issue ```dafny datatype Option = | None | Some(val: nat) datatype Test = Test( field: Option ) ghost predicate UpdateField(t: Test,...

Using `:|` operator to create a set with a forall condition results in Boogie internal error

1

### Dafny version 4.9.1.0 ### Code to produce this issue ```dafny ghost predicate trigger1(x : nat) { true } lemma Break() { // line below causes internal error var x...

feat: Implementing Mutual Fixpoints

4

Implementation for issue #46 Ported the [`fixpointAB`](https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.ofe.html#fixpointAB) and [`fixpointAB_ne`](https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.ofe.html#fixpointAB_ne) sections from the Rocq implementation.