refactor(init/meta/lean/parser): simplify sep_by

This commit is contained in:
Sebastian Ullrich 2017-02-23 01:31:44 +01:00
parent dd379e5b34
commit 8c50efeb75

View file

@ -57,11 +57,10 @@ meta def {u v} many {f : Type u → Type v} [monad f] [alternative f] {a : Type
return $ y::ys) <|> pure list.nil
local postfix ?:100 := optional
local notation p ` ?: `:100 d := (λ o, option.get_or_else o d) <$> p?
local postfix * := many
meta def sep_by {α : Type} : string → parser α → parser (list α)
| s p := (list.cons <$> p <*> (tk s *> p)*) ?: []
| s p := (list.cons <$> p <*> (tk s *> p)*) <|> return []
end parser
end lean