def Hex.Perm.ofImages (n : Nat) (l : List Nat) : Perm n

A permutation from its literal image list, with identity as the fallback for invalid input. Kernel.ofNatArray_permOfImages proves this fallback is unreachable when Kernel.imagesOk accepts.

Equations

• Hex.Perm.ofImages n l = match Hex.Perm.ofNatArray? n l.toArray with | some p => p | none => Hex.Perm.id n

def Hex.Perm.images {n : Nat} (p : Perm n) : List Nat

The image list, read by the tactic in compiled code.

Equations

• p.images = List.map (fun (i : Fin n) => ↑(p.get i)) (List.finRange n)