A
and an equivalence relation on A
.It looks like :theories/Setoids/Setoid.v
Section Setoid. Variable A : Type. Variable Aeq : A -> A -> Prop. Record Setoid_Theory : Prop := { Seq_refl : (x:A) (Aeq x x); Seq_sym : (x,y:A) (Aeq x y) -> (Aeq y x); Seq_trans : (x,y,z:A) (Aeq x y) -> (Aeq y z) -> (Aeq x z) }.
A
, you must provide a relation
Aeq
on A
and prove that Aeq
is an equivalence
relation. That is, you have to define an object of type
(Setoid_Theory A Aeq)
.Add Setoid A Aeq STwhere Aeq is a term of type A->A->Prop and ST is a term of type (Setoid_Theory A Aeq).
Add Morphism f : identwhere f is the name of a term which type is a non dependent product (the term you want to declare as a morphism) and ident is a new identifier which will denote the compatibility lemma.
setoid_replace term_{1} with term_{2}The effect is similar to the one of replace.
setoid_rewrite term