Path Definition

Definition of a path in ListST. Given a list of Tokens [t_1, .. , t_n] (we represent tokens as their IDs.), they are a path if and only if each token is a token (in our representation, that means their ID is a valid id.) and [t_i, t_(i.succ)] for i ∈ [1,n_1].

def Paths.Definitions.bisPath {α : Type} (ls : List Tokens.Elem.TId) (s : MUList.State.ListST α) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Paths.Definitions.bisPath [] s = true
• Paths.Definitions.bisPath [y] s = (Tokens.State.Tokens.get y s).isSome

def Paths.Definitions.isPath {α : Type} (ls : List Tokens.Elem.TId) (s : MUList.State.ListST α) : Prop

Equations

• One or more equations did not get rendered due to their size.
• Paths.Definitions.isPath [] s = True
• Paths.Definitions.isPath [y] s = ((Tokens.State.Tokens.get y s).isSome = true)