def Iris.Instances.Classical.maps_to {Val : Type u_1} (l : Nat) (v : Val) : HeapProp Val

Equations

• iprop(l ↦ v) state = (state l = Iris.Instances.Data.result v)

def Iris.Instances.Classical.«term_↦_» : Lean.TrailingParserDescr

State that a heap cell contains a certain value.

Equations

• One or more equations did not get rendered due to their size.