Zulip Chat Archive
Stream: iris-lean
Topics:
- Iris-Lean demos (5 messages, latest: Feb 05 2026 at 14:16)
- Why are sForall and sExists defined the way they are? (16 messages, latest: Feb 03 2026 at 15:00)
- Noting Rocq names when porting (1 message, latest: Jan 29 2026 at 15:41)
- New tasks: PORTING.md (13 messages, latest: Jan 29 2026 at 11:41)
- Acknowledge Iris Rocq License? (3 messages, latest: Jan 26 2026 at 13:19)
- stdpp (73 messages, latest: Jan 26 2026 at 02:32)
- specialization pattern syntax (26 messages, latest: Jan 10 2026 at 16:41)
- Hoare Triples in Iris-Lean (16 messages, latest: Jan 09 2026 at 15:29)
- Bi-entailment and generalized rewriting (4 messages, latest: Dec 25 2025 at 03:13)
- Chaining CoeFun instances? (1 message, latest: Dec 20 2025 at 05:48)
- proof mode terms for icases (36 messages, latest: Dec 17 2025 at 13:46)
- Mutual Fixpoints (Beginner Contributor Questions) (12 messages, latest: Dec 15 2025 at 21:03)
- Issues with typeclasses in the proof mode (18 messages, latest: Dec 12 2025 at 08:13)
- Next steps (71 messages, latest: Dec 02 2025 at 16:51)
- transfinite step indexing? (6 messages, latest: Dec 02 2025 at 00:04)
- Ltac2 (29 messages, latest: Dec 01 2025 at 16:46)
- pure propositions (6 messages, latest: Nov 26 2025 at 16:52)
- Iris-Lean at NJPLS (1 message, latest: Nov 25 2025 at 16:04)
- Who wants the glory of finishing iProp? (29 messages, latest: Nov 23 2025 at 20:28)
- iApply tactic implemented (42 messages, latest: Oct 27 2025 at 12:25)
- Porting iris-tutorial (8 messages, latest: Oct 24 2025 at 15:02)
- Merging PRs (30 messages, latest: Oct 15 2025 at 10:58)
- Porting iProp to typeclasses (71 messages, latest: Oct 10 2025 at 19:57)
- Heaplang (20 messages, latest: Sep 26 2025 at 22:21)
- iris-lean docs (8 messages, latest: Aug 06 2025 at 14:40)
- Data structure for sets (16 messages, latest: Aug 04 2025 at 13:51)
- Rationals needed for the Frac CMRA? (313 messages, latest: Jul 29 2025 at 19:50)
- Next milestone: Iris 0.5 ("Monoids are all you need!") (58 messages, latest: Jul 19 2025 at 18:10)
- Looking for feedback on gmap generalization (55 messages, latest: Jul 18 2025 at 19:11)
- Minor UX quibble (31 messages, latest: Jul 18 2025 at 15:37)
- Toolchain Update (1 message, latest: Jul 18 2025 at 13:15)
- Rocq Iris repo inaccessible (4 messages, latest: Jul 18 2025 at 06:19)
- Unicode symbol for
-*(16 messages, latest: Jul 17 2025 at 15:59) - NML (10 messages, latest: Jul 17 2025 at 06:40)
- The Numbers CMRA (40 messages, latest: Jul 08 2025 at 17:07)
- Why are Hyps a tree instead of a list? (21 messages, latest: Jul 07 2025 at 20:47)
- iRevert implementation and Qq (7 messages, latest: Jul 05 2025 at 11:12)
- Tactics discussion (37 messages, latest: Jul 03 2025 at 13:17)
- Iris 4.4 (3 messages, latest: Jul 03 2025 at 12:14)
- Universe bug in product CMRA? (6 messages, latest: Jun 23 2025 at 21:41)
- Understanding and Porting O/RFunctors (9 messages, latest: Jun 12 2025 at 14:41)
- Update and switch to lakefile.toml (91 messages, latest: May 15 2025 at 13:40)
- Good first issues for new contibutors? (49 messages, latest: May 14 2025 at 20:42)
pcore_monovspcore_mono'(23 messages, latest: Apr 13 2025 at 16:44)- Figuring out the OFunctor hierarchy (8 messages, latest: Apr 09 2025 at 13:15)
- OFunctor definition (19 messages, latest: Apr 05 2025 at 21:17)
- Use of mathlib? (14 messages, latest: Mar 17 2025 at 21:43)
- channel events (1 message, latest: Mar 12 2025 at 16:20)
Last updated: Feb 28 2026 at 14:05 UTC