FinMatrix.CoqExt.TupleExt


Open Scope type_scope.

Short name for tuples type

Section TuplesType.

  Context {A : Type}.

  Definition T2 := A * A.
  Definition T3 := T2 * A.
  Definition T4 := T3 * A.

  Definition T_2_2 := T2 * T2.
  Definition T_3_3 := T3 * T3 * T3.

End TuplesType.