refactor(library/init/list): move list notation to the top-level
This commit is contained in:
parent
586baa4118
commit
7e15b114e6
1 changed files with 2 additions and 1 deletions
|
|
@ -25,10 +25,11 @@ list.rec_on l₁
|
|||
(λ Hne : l₁ ≠ l₂, ff (λ H, list.no_confusion H (λ Hab Hl₁l₂, absurd Hl₁l₂ Hne)))
|
||||
(λ He : l₁ = l₂, tt (congr (congr_arg cons Hab) He)))))
|
||||
|
||||
namespace list
|
||||
notation h :: t := cons h t
|
||||
notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
|
||||
|
||||
namespace list
|
||||
|
||||
variable {A : Type}
|
||||
|
||||
definition append : list A → list A → list A
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue