The paper Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic talks about defining "Iris Inductives". I think this would be a great feature to add to core Iris-Lean. Here's an illustrative example from the paper translated into Lean-y syntax:
iinductive IsListWithTail (tl : loc) : loc → list val → iProp GF where
| nil : tl ↦ NIL -∗ IsListWithTail tl tl []
| cons {v vs l l'} : l ↦ CONS (v,#l') -∗ IsListWithTail tl l' vs -∗ IsListWithTail tl l (v :: vs)
| del {vs l l'} : l ↦ #l' -∗ IsListWithTail tl l' vs -∗ IsListWithTail tl l vsI think we have all the theory for this, though getting an iinductive which behaves like a Lean inductive includes plenty of corner cases that would need some care. I'm similarly curious if we might be able to write a nice version of istructure-- I'd expect that to be a lot easier.
The paper Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic talks about defining "Iris Inductives". I think this would be a great feature to add to core Iris-Lean. Here's an illustrative example from the paper translated into Lean-y syntax:
iinductive IsListWithTail (tl : loc) : loc → list val → iProp GF where | nil : tl ↦ NIL -∗ IsListWithTail tl tl [] | cons {v vs l l'} : l ↦ CONS (v,#l') -∗ IsListWithTail tl l' vs -∗ IsListWithTail tl l (v :: vs) | del {vs l l'} : l ↦ #l' -∗ IsListWithTail tl l' vs -∗ IsListWithTail tl l vsI think we have all the theory for this, though getting an
iinductivewhich behaves like a Leaninductiveincludes plenty of corner cases that would need some care. I'm similarly curious if we might be able to write a nice version ofistructure-- I'd expect that to be a lot easier.