From e585be6db5fef21d0a4e7cb5371fd218566a05e5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 May 2018 13:42:12 +0200
Subject: [PATCH] Remove the `default` notation for options

The notation was parsing-only and all it did was reorder the arguments for
from_option.  This creates just a needless divergence between what is written
and what is printed.  Also, removing it frees the name for maybe introducing a
function or notation `default` with a type like `T -> option T -> T`.
---
 theories/nmap.v    | 2 +-
 theories/option.v  | 4 ----
 theories/pmap.v    | 2 +-
 theories/strings.v | 2 +-
 theories/zmap.v    | 2 +-
 5 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/theories/nmap.v b/theories/nmap.v
index 8ab9fa87..7e56c562 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -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.
diff --git a/theories/option.v b/theories/option.v
index fa3fbd61..6d82eed0 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -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.
diff --git a/theories/pmap.v b/theories/pmap.v
index 0eba03ef..519641c2 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -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 :=
diff --git a/theories/strings.v b/theories/strings.v
index d7ba9adb..2110270a 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -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.
 
diff --git a/theories/zmap.v b/theories/zmap.v
index 241b1d3c..31177c02 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -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.
-- 
GitLab