lean4-htt/tests
Leonardo de Moura d0ade7ff08 feat: extend doBlock expander
- Add support for `if h:c then t else e`, `h` may shadow reassignable
variables

- Pattern variables in `match` alternatives may shadow reassignable
variables

- A single declaration/reassignment in a `do` block may
declare/reassign multiple variables. Example: `let (x, y) := t`
2020-10-01 10:40:55 -07:00
..
bench chore: fix stdlib benchmark 2020-09-28 13:39:32 +02:00
compiler chore: fix test 2020-09-28 17:11:00 -07:00
elabissues chore: fix syntax 2020-05-21 09:57:35 -07:00
ir chore(tests): fix do syntax in tests 2019-06-30 13:04:34 +02:00
lean feat: extend doBlock expander 2020-10-01 10:40:55 -07:00
playground test: optional ';' 2020-09-28 17:11:00 -07:00
plugin chore: remove comment from Linter 2020-06-17 21:28:03 -07:00
.gitignore chore: move bin/ and .oleans into build directory 2020-05-14 14:47:54 +02:00
common.sh test: ignore \r when diffing 2020-09-15 09:32:00 -07:00