lean4-htt/library/init/data
Leonardo de Moura 38bc3beffb fix(library/init): alternative instances
Both `alternative` and `monad` implement `applicative`. However,
their default implementations for `seq_right` and `seq_left` are
different. The `alternative` implementation uses the inefficient default
version for `seq_right` available at `applicative`:
```
(seq_right := λ α β a b, const α id <$> a <*> b)
```
instead of the more efficient
```
(seq_right := λ α β x y, x >>= λ _, y)
```
defined at `monad` using the `bind` operator.

This commit makes sure the `applicative` instances for `reader_t`,
`state_t`, `option` and `parsec_t` use the efficient version.
I found the problem when inspecting the generated code for:
```
def symbol (s : string) : parsec' unit :=
(str s *> whitespace) <?> ("'" ++ s ++ "'")
```
2018-10-17 14:25:50 -07:00
..
array perf(library/init/data): mark usize, uint16, uint32 and uint64 as [irreducible] 2018-05-07 18:07:04 -07:00
char chore(library/init): missing [inline] and remove unnecessary defs 2018-10-17 08:38:30 -07:00
fin feat(library/init/core): decidable_eq is a proper class 2018-09-07 16:38:11 -07:00
hashmap fix(frontends/lean/elaborator): ensure_no_unassigned_metavars: only check mvars in parameter 2018-10-07 21:11:02 -07:00
int feat(library/init/core): decidable_eq is a proper class 2018-09-07 16:38:11 -07:00
list chore(library/init): mark a few combinators with [specialize] 2018-10-15 13:47:26 -07:00
nat chore(library/init/data/nat/basic): missing @[inline] 2018-10-03 17:24:53 -07:00
option fix(library/init): alternative instances 2018-10-17 14:25:50 -07:00
ordering chore(library/init/data/ordering/basic): mark cmp_using as [inline] 2018-09-17 14:56:31 -07:00
rbmap chore(library): remove >>, we should use *> 2018-09-12 17:31:21 -07:00
rbtree chore(library): remove >>, we should use *> 2018-09-12 17:31:21 -07:00
string chore(library/init/string): remove string.iterator_imp 2018-10-02 13:46:01 -07:00
basic.lean chore(*): remove more files 2018-05-21 06:42:58 -07:00
default.lean chore(*): remove several tactics 2018-05-21 06:53:01 -07:00
dlist.lean feat(library/init/data/dlist): inlining dlist functions is counterproductive 2018-09-24 18:47:10 -07:00
hashable.lean feat(library/init/data/hashable): add hashable nat instance 2018-05-06 07:53:29 -07:00
repr.lean chore(library/init/data/repr): remove unnecessary definition 2018-10-17 12:32:38 -07:00
to_string.lean chore(library/init/data/to_string): remove unnecessary definition 2018-10-16 16:18:07 -07:00
uint.lean feat(library/init/data/uint): add uint8 2018-10-01 14:17:11 -07:00
usize.lean perf(library/init/data): mark usize, uint16, uint32 and uint64 as [irreducible] 2018-05-07 18:07:04 -07:00