max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/data/dlist): add @[inline]

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-07 09:58:53 -07:00
parent 79f351d177
commit 5b89f69e36
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/init/data/dlist.lean
View file

@ -20,19 +20,19 @@ namespace dlist
variables {α : Type u}
open list
def of_list (l : list α) : dlist α :=
@[inline] def of_list (l : list α) : dlist α :=
⟨append l, λ t, (append_nil l).symm ▸ rfl⟩
def empty : dlist α :=
@[inline] def empty : dlist α :=
⟨id, λ t, rfl⟩
def to_list : dlist α → list α
@[inline] def to_list : dlist α → list α
| ⟨f, h⟩ := f []
def singleton : α → dlist α
| a := ⟨λ t, a :: t, λ t, rfl⟩
@[inline] def singleton (a : α) : dlist α :=
⟨λ t, a :: t, λ t, rfl⟩
def cons : α → dlist α → dlist α
@[inline] def cons : α → dlist α → dlist α
| a ⟨f, h⟩ := ⟨λ t, a :: f t, λ t,
show a :: f t = a :: (f [] ++ t), from h t ▸ rfl⟩