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

Equations

• Paths.Utils.fromPath [] s HPath_2 = []
• Paths.Utils.fromPath [y] s HPath_2 = match H : Tokens.State.Tokens.get y s with | none => ⋯.elim | some y' => [y']
• Paths.Utils.fromPath (y :: y' :: ys) s HPath_2 = match H : Tokens.State.Tokens.get y s with | none => ⋯.elim | some nd_y => nd_y :: Paths.Utils.fromPath (y' :: ys) s ⋯

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

Equations

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

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

Equations

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