CoRN.model.metric2.CRmetric

Require Export Complete.
Require Export Prelength.
Require Import Qmetric.
Require Import CornTac.
Require Import canonical_names.
Require Import stdlib_rationals.

Set Implicit Arguments.

Open Local Scope uc_scope.

Complete Metric Space: Computable Reals (CR)

Definition CR := Complete Q_as_MetricSpace.

Delimit Scope CR_scope with CR.
Bind Scope CR_scope with CR.

Instance inject_Q_CR: Cast Q CR := (@Cunit Q_as_MetricSpace).

Notation "' x" := (inject_Q_CR x) : CR_scope.

Notation "x == y" := (@st_eq CR x y) (at level 70, no associativity) : CR_scope.