Commit d61ed9a8 authored by Robbert Krebbers's avatar Robbert Krebbers

Get rid of some deprecated notations.

parent bd4a6a84
Pipeline #7339 passed with stage
in 13 minutes and 49 seconds
......@@ -37,9 +37,9 @@ Section choice.
Context `{Countable A} (P : A Prop).
Inductive choose_step: relation positive :=
| choose_step_None {p} : decode (A:=A) p = None choose_step (Psucc p) p
| choose_step_None {p} : decode (A:=A) p = None choose_step (Pos.succ p) p
| choose_step_Some {p} {x : A} :
decode p = Some x ¬P x choose_step (Psucc p) p.
decode p = Some x ¬P x choose_step (Pos.succ p) p.
Lemma choose_step_acc : ( x, P x) Acc choose_step 1%positive.
Proof.
intros [x Hx]. cut ( i p,
......
......@@ -223,10 +223,10 @@ Proof. by injection 1. Qed.
Instance N_eq_dec: EqDecision N := N.eq_dec.
Program Instance N_le_dec : RelDecision N.le := λ x y,
match Ncompare x y with Gt => right _ | _ => left _ end.
match N.compare x y with Gt => right _ | _ => left _ end.
Solve Obligations with naive_solver.
Program Instance N_lt_dec : RelDecision N.lt := λ x y,
match Ncompare x y with Lt => left _ | _ => right _ end.
match N.compare x y with Lt => left _ | _ => right _ end.
Solve Obligations with naive_solver.
Instance N_inhabited: Inhabited N := populate 1%N.
Instance N_le_po: PartialOrder ()%N.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment