The Iris Tutorial in Lean

21. Defining Resource Algebras from Scratch🔗

This chapter has not yet been ported. The Rocq source is iris-tutorial/theories/custom_ra.v.