From 425b5ffc11ca5ff2d03d67ffc1b194fd2a6ed39d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Mar 2017 18:09:32 -0800
Subject: [PATCH] chore(library/data/dlist): make local notation less cryptic

---
 library/data/dlist.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/library/data/dlist.lean b/library/data/dlist.lean
index 0a2924b135..cf1d9fc3b3 100644
--- a/library/data/dlist.lean
+++ b/library/data/dlist.lean
@@ -33,21 +33,21 @@ def to_list : dlist α → list α
 def empty : dlist α :=
 ⟨id, ♯⟩
 
-local notation a `:::`:max := list.cons a
+local notation a `::_`:max := list.cons a
 
 /-- Create dlist with a single element -/
 def singleton (x : α) : dlist α :=
-⟨x:::, ♯⟩
+⟨x::_, ♯⟩
 
 local attribute [simp] function.comp
 
 /-- `O(1)` Prepend a single element to a dlist -/
 def cons (x : α) : dlist α →  dlist α
-| ⟨xs, h⟩ := ⟨x::: ∘ xs, ♯⟩
+| ⟨xs, h⟩ := ⟨x::_ ∘ xs, ♯⟩
 
 /-- `O(1)` Append a single element to a dlist -/
 def concat (x : α) : dlist α → dlist α
-| ⟨xs, h⟩ := ⟨xs ∘ x:::, ♯⟩
+| ⟨xs, h⟩ := ⟨xs ∘ x::_, ♯⟩
 
 /-- `O(1)` Append dlists -/
 protected def append : dlist α → dlist α → dlist α