We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 71f9cb8 commit 3e616d0Copy full SHA for 3e616d0
theories/Algebra/Universal/TermAlgebra.v
@@ -30,7 +30,7 @@ Inductive CarriersTermAlgebra {σ} (C : Carriers σ) : Carriers σ :=
30
DomOperation (CarriersTermAlgebra C) (σ u) ->
31
CarriersTermAlgebra C (sort_cod (σ u)).
32
33
-Scheme CarriersTermAlgebra_ind := Elimination for CarriersTermAlgebra Sort Type.
+Scheme CarriersTermAlgebra_ind := Induction for CarriersTermAlgebra Sort Type.
34
Arguments CarriersTermAlgebra_ind {σ}.
35
36
Definition CarriersTermAlgebra_rect {σ} := @CarriersTermAlgebra_ind σ.
0 commit comments