- in_start {es : Spec.Entities} {start : Data.Set Spec.EntityUID} {finish : Spec.EntityUID} {level : Nat} (hs : finish ∈ start) : ReachableIn es start finish (level + 1)
- step {es : Spec.Entities} {start : Data.Set Spec.EntityUID} {finish : Spec.EntityUID} {level : Nat} {ed : Spec.EntityData} (i : Spec.EntityUID) (hi : i ∈ start) (he : Data.Map.find? es i = some ed) (hr : ReachableIn es ed.sliceEUIDs finish level) : ReachableIn es start finish (level + 1)
Instances For
- euid (euid : Spec.EntityUID) : EuidViaPath (Spec.Value.prim (Spec.Prim.entityUID euid)) [] euid
- record {v : Spec.Value} {euid : Spec.EntityUID} {a : Spec.Attr} {path : List Spec.Attr} {attrs : Data.Map Spec.Attr Spec.Value} (ha : attrs.find? a = some v) (hv : EuidViaPath v path euid) : EuidViaPath (Spec.Value.record attrs) (a :: path) euid
Instances For
theorem
Cedar.Thm.in_val_then_val_slice
{v : Spec.Value}
{path : List Spec.Attr}
{euid : Spec.EntityUID}
(hv : Value.EuidViaPath v path euid)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[irreducible]
theorem
Cedar.Thm.reachable_succ
{n : Nat}
{euid : Spec.EntityUID}
{start : Data.Set Spec.EntityUID}
{entities : Spec.Entities}
(hr : ReachableIn entities start euid n)
:
ReachableIn entities start euid (n + 1)
theorem
Cedar.Thm.entities_attrs_then_find?
{entities : Spec.Entities}
{attrs : Data.Map Spec.Attr Spec.Value}
{uid : Spec.EntityUID}
(he : entities.attrs uid = Except.ok attrs)
:
theorem
Cedar.Thm.entities_tags_then_find?
{entities : Spec.Entities}
{tags : Data.Map Spec.Tag Spec.Value}
{uid : Spec.EntityUID}
(he : entities.tags uid = Except.ok tags)
: