ROSCOQ.CanonicalNotations
Class SqrtFun (A B : Type) := sqrtFun : A → B.
Notation "√" := sqrtFun.
Class RealNumberPi (R : Type) := π : R.
Class HalfNum (R : Type) := half_num : R.
Notation "½" := half_num.
Notation "√" := sqrtFun.
Class RealNumberPi (R : Type) := π : R.
Class HalfNum (R : Type) := half_num : R.
Notation "½" := half_num.
Should we add other properties of distance, e.g. triangle inequality?
Class NormSpace (A B : Type) := norm : A → B.
Notation "| x |" := (norm x) (at level 300).
Class ProjectionFst (Prod A : Type) := π₁ : Prod → A.
Instance ProjectionFst_instance_prod (A B : Type) :
ProjectionFst (prod A B) A := (@fst A B) .
Instance ProjectionFst_instance_conj (A B : Prop) :
ProjectionFst (A ∧ B) A := (@proj1 A B) .
Notation "| x |" := (norm x) (at level 300).
Class ProjectionFst (Prod A : Type) := π₁ : Prod → A.
Instance ProjectionFst_instance_prod (A B : Type) :
ProjectionFst (prod A B) A := (@fst A B) .
Instance ProjectionFst_instance_conj (A B : Prop) :
ProjectionFst (A ∧ B) A := (@proj1 A B) .