Documentation

Init.Grind.Homo.List

Imports

Init.Grind.Attr
Init.Data.List.Erase
Init.Data.List.Lemmas
Init.Data.List.TakeDrop
Init.Data.List.Zip
Init.Data.List.Nat.InsertIdx
Init.Data.List.Nat.Modify
Init.Data.List.Nat.TakeDrop

Imported by

← Mathematical handbook

Homomorphism rules for List used by the grind tactic. The injection function is List.length.