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

chore: missing annotations at List.mapTR

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-27 10:17:49 -07:00
parent 8ba10521e6
commit b205cfaaf2
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/List/Basic.lean
View file

@ -100,11 +100,11 @@ def isEmpty : List α → Bool
| [] => []
| a::as => f a :: map f as
def mapTRAux (f : α → β) : List α → List β → List β
@[specialize] def mapTRAux (f : α → β) : List α → List β → List β
| [], bs => bs.reverse
| a::as, bs => mapTRAux f as (f a :: bs)
def mapTR (f : α → β) (as : List α) : List β :=
@[inline] def mapTR (f : α → β) (as : List α) : List β :=
mapTRAux f as []
theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux as [] ++ bs := by