Lean4
/-- Basic meta-code "normal form" object of the `match_scalars` and `module` tactics: a type synonym
for a list of ordered triples comprising expressions representing terms of two types `R` and `M`
(where typically `M` is an `R`-module), together with a natural number "index".
The natural number represents the index of the `M` term in the `AtomM` monad: this is not enforced,
but is sometimes assumed in operations. Thus when items `((a₁, x₁), k)` and `((a₂, x₂), k)`
appear in two different `Module.qNF` objects (i.e. with the same `ℕ`-index `k`), it is expected that
the expressions `x₁` and `x₂` are the same. It is also expected that the items in a `Module.qNF`
list are in strictly increasing order by natural-number index.
By forgetting the natural number indices, an expression representing a `Mathlib.Tactic.Module.NF`
object can be built from a `Module.qNF` object; this construction is provided as
`Mathlib.Tactic.Module.qNF.toNF`. -/
abbrev qNF (R : Q(Type u)) (M : Q(Type v)) :=
List ((Q($R) × Q($M)) × ℕ)
