Structural permutations

In this file, we define the type of structural permutations.

Main declarations

• ConNF.StrPerm: The type of structural permutations.

@[reducible, inline]

abbrev ConNF.StrPerm [Params] : TypeIndex → Type u

Equations

• ConNF.StrPerm = ConNF.Tree ConNF.BasePerm