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

feat(library/init/lean/parser/parsec): missing [inline]

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-24 18:57:49 -07:00
parent 1f42b5bce9
commit b4b42ef8b2
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/parser/parsec.lean
View file

@ -168,7 +168,7 @@ together.
```
Without the `try` combinator we will not be able to backtrack on the `let` keyword.
-/
def try (p : parsec_t μ m α) : parsec_t μ m α :=
@[inline] def try (p : parsec_t μ m α) : parsec_t μ m α :=
λ it, do
r ← p it,
pure $ match r with
@ -187,7 +187,7 @@ def try (p : parsec_t μ m α) : parsec_t μ m α :=
combine their error messages (even if one of
them succeeded).
-/
protected def orelse (p q : parsec_t μ m α) : parsec_t μ m α :=
@[inline] protected def orelse (p q : parsec_t μ m α) : parsec_t μ m α :=
λ it, do
r ← p it,
match r with