Commit de797b31 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/default' into 'master'

Remove the `default` notation for options

See merge request robbertkrebbers/coq-stdpp!31
parents a8f65af5 e585be6d
......@@ -35,7 +35,7 @@ Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
match t with
| NMap o t =>
default [] o (λ x, [(0,x)]) ++ (prod_map Npos id <$> map_to_list t)
from_option (λ x, [(0,x)]) [] o ++ (prod_map Npos id <$> map_to_list t)
end.
Instance Nomap: OMap Nmap := λ A B f t,
match t with NMap o t => NMap (o = f) (omap f t) end.
......
......@@ -26,10 +26,6 @@ Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
Instance: Params (@from_option) 3.
Arguments from_option {_ _} _ _ !_ / : assert.
(* The eliminator again, but with the arguments in different order, which is
sometimes more convenient. *)
Notation default y mx f := (from_option f y mx) (only parsing).
(** An alternative, but equivalent, definition of equality on the option
data type. This theorem is useful to prove that two options are the same. *)
Lemma option_eq {A} (mx my: option A): mx = my x, mx = Some x my = Some x.
......
......@@ -86,7 +86,7 @@ Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A)
(acc : list (positive * A)) : list (positive * A) :=
match t with
| PLeaf => acc
| PNode o l r => default [] o (λ x, [(Preverse j, x)]) ++
| PNode o l r => from_option (λ x, [(Preverse j, x)]) [] o ++
Pto_list_raw (j~0) l (Pto_list_raw (j~1) r acc)
end%list.
Fixpoint Pomap_raw {A B} (f : A option B) (t : Pmap_raw A) : Pmap_raw B :=
......
......@@ -57,7 +57,7 @@ Fixpoint words_go (cur : option string) (s : string) : list string :=
| "" => option_list (string_rev <$> cur)
| String a s =>
if is_space a then option_list (string_rev <$> cur) ++ words_go None s
else words_go (Some (default (String a "") cur (String a))) s
else words_go (Some (from_option (String a) (String a "") cur)) s
end.
Definition words : string list string := words_go None.
......
......@@ -35,7 +35,7 @@ Instance Zpartial_alter {A} : PartialAlter Z A (Zmap A) := λ f i t,
end.
Instance Zto_list {A} : FinMapToList Z A (Zmap A) := λ t,
match t with
| ZMap o t t' => default [] o (λ x, [(0,x)]) ++
| ZMap o t t' => from_option (λ x, [(0,x)]) [] o ++
(prod_map Zpos id <$> map_to_list t) ++
(prod_map Zneg id <$> map_to_list t')
end.
......
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