max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/run
History
Leonardo de Moura 6625656940 refactor: remove support for fun {a : A} => ... 
The semantics was weird. It seems Agda is also having problems with
it. Here is an example that demonstrates how weird the semantics is:

```lean
check (fun {β α} (a : α) (b : β) => (b, a) : {α : Type} → {β : Type} → (a : α) → (b : β) → β × α)

-- Same example using `def`
def f : {α : Type} → {β : Type} → α → β → β × α :=
fun {β : Type} {α : Type} (a : α) (b : β) => (b, a)
```

Both commands were being accepted before this commit. Note that it
flips `β` and `α`.

Here is an example that did not work before this commit and would
confuse users.

```lean
check
  let id := fun {α} (a : α) => a;
  id [id 1]
```

users would have to write

```lean
check
  let id {α} (a : α) := a;
  id [id 1]
```

@Kha The Delaborator.lean test broke and I "fixed" by removing the
`{}` from it, and copying `produced` over `expected`. Please make sure
it still makes sense.
2020-03-26 10:40:16 -07:00
..
.gitignore chore: ignore test output files 2020-01-27 13:08:57 +01:00
28.lean fix(library/init/data/persistentarray/basic): bug at pop 2019-08-14 16:14:20 -07:00
34.lean chore: fix tests 2019-11-05 14:44:05 -08:00
108.lean fix: closes #108 2020-02-01 23:17:00 -08:00
111.lean fix: closes #111 2020-01-30 14:09:47 -08:00
121.lean fix: #121 in the old frontend 2020-03-06 13:43:19 -08:00
125.lean fix: bug at unsafe umapMAux implementation 2020-03-14 13:41:14 -07:00
1954.lean chore(tests): fix tests 2019-06-24 15:48:11 -07:00
1968.lean chore(frontends/lean): fun x, e ==> fun x => e 2019-07-02 13:22:11 -07:00
anonymous_ctor_error_msg.lean doc: document issue 2020-02-18 10:41:12 -08:00
array1.lean feat: add forRevM 2019-12-19 17:24:29 -08:00
autoparam.lean feat: elaborate autoParams 2020-02-13 16:24:50 -08:00
backtrackable_estate.lean chore: fix tests 2019-11-05 14:44:05 -08:00
bigmul.lean fix: assertion violation 2020-01-31 08:25:59 -08:00
bigop.lean feat: antiquotation escapes 2020-02-18 10:57:12 -08:00
borrowBug.lean test: minimal repro for Borrow.lean bug 2019-12-22 19:16:23 -08:00
check.lean refactor: remove Expr.mvar hidden field 2019-11-15 10:04:42 -08:00
choiceMacroRules.lean test: overload builtin notation 2020-01-26 14:00:41 -08:00
closure1.lean feat: add tests for Closure.lean 2020-03-20 18:32:04 -07:00
coeIssue1.lean feat: add coercion tests 2020-01-28 15:52:04 -08:00
coeIssue2.lean feat: add coercion tests 2020-01-28 15:52:04 -08:00
coeIssue3.lean feat: add coercion tests 2020-01-28 15:52:04 -08:00
coeIssues4.lean feat: add bridge Coe + HasNat transitivity instance 2020-01-28 16:17:14 -08:00
CoeNew.lean feat: simplify Coe again 2020-01-29 22:08:42 -08:00
coeSort1.lean feat: simplify CoeFun and CoeSort 2020-01-29 21:56:26 -08:00
coeSort2.lean feat: simplify CoeFun and CoeSort 2020-01-29 21:56:26 -08:00
CommandExtOverlap.lean feat: add elabChoice for CommandElab 2020-02-18 17:18:28 -08:00
compiler_proj_bug.lean chore(tests/lean/extract): reactivate some #eval tests 2019-09-19 18:12:51 +02:00
constantCompilerBug.lean refactor: remove ParserKind 2020-01-30 20:56:46 -08:00
coroutine.lean chore: fix test 2020-02-10 14:48:57 -08:00
csimp_type_error.lean chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
DefEqAssignBug.lean fix: isDefEqQuick 2019-12-19 11:10:58 -08:00
deriv.lean fix: file and import names, tests and stage0 2019-10-04 17:04:02 -07:00
doNotation1.lean chore: remove unncessary annotation 2020-02-04 14:21:26 -08:00
elabIte.lean feat: change ite and dite argument order 2020-02-03 14:11:29 -08:00
etaFirst.lean test: unifier 2020-03-05 18:44:33 -08:00
eval_unboxed_const.lean fix: interpreter::call_boxed on unboxed constants 2020-03-14 15:04:38 -07:00
evalconst.lean test: minimal repro for evalConst crash 2020-01-01 11:02:38 -08:00
expectedTypePropagation.lean fix: forget to update 2020-01-29 20:08:03 -08:00
expr1.lean feat: file IO using handles 2020-01-12 08:02:48 -08:00
expr_maps.lean feat: file IO using handles 2020-01-12 08:02:48 -08:00
ext_eff.lean chore(frontends/lean): fun x, e ==> fun x => e 2019-07-02 13:22:11 -07:00
ext_eff_linear.lean chore(frontends/lean): fun x, e ==> fun x => e 2019-07-02 13:22:11 -07:00
extern.lean chore(tests): port tests, fix at least compiler tests 2019-03-21 15:11:05 -07:00
extmacro.lean test: add extensible macro example 2020-01-21 14:05:21 -08:00
float_cases_bug.lean chore: fix tests 2020-01-28 10:34:27 -08:00
foldConsts.lean feat: add Expr.foldConsts 2020-03-16 14:33:30 -07:00
frontend1.lean refactor: remove ParserKind 2020-01-30 20:56:46 -08:00
fun.lean chore: fix tests 2019-11-05 14:44:05 -08:00
generalize.lean feat: finish evalGeneralize 2020-02-21 18:32:00 -08:00
generalizeTelescope.lean test: generalizeTelescope tests 2020-03-25 16:00:55 -07:00
genindices.lean feat: add generalizeIndices 2020-03-04 16:27:01 -08:00
getline_crash.lean chore: fix test 2020-03-23 15:47:51 -07:00
handlers.lean fix: file and import names, tests and stage0 2019-10-04 17:04:02 -07:00
ind_cmd_bug.lean
induction1.lean test: new tests 2020-03-05 18:44:33 -08:00
inj1.lean test: injection tactic tests 2020-03-08 17:45:58 -07:00
inj2.lean test: add dependent elimination tests 2020-03-09 15:12:07 -07:00
inline_fn.lean chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
inliner_loop.lean chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
instances.lean chore: fix test 2019-12-02 19:42:44 -08:00
instuniv.lean chore: fix tests 2019-12-15 18:34:13 -08:00
int_to_nat_bug.lean fix: lean_nat_abs 2019-12-14 08:08:41 -08:00
IO_test.lean feat: add IO.FS.lines 2020-03-23 14:53:27 -07:00
kernel1.lean test: reduceBool test 2020-03-14 15:07:14 -07:00
kernel2.lean test: decide! tests 2020-03-18 16:48:28 -07:00
kevin.lean feat: elaborate quoted names 2020-01-19 11:58:17 -08:00
level.lean chore: fix tests 2019-11-17 08:53:18 -08:00
LiftMethodIssue.lean chore: fix test 2020-02-11 16:26:39 -08:00
listDecEq.lean feat: add withPtrEqDecEq (version of withPtrEq for implementing decidable equality) 2020-02-15 16:12:09 -08:00
macro.lean chore: use new_frontend in the whole test 2020-01-21 09:16:38 -08:00
macro2.lean chore: test 2020-01-20 18:53:54 -08:00
macro3.lean feat: add Array.getSepElems 2020-01-18 19:12:44 -08:00
macro_macro.lean fix: add workaround for setting correct LBP for $ in antiquotations 2020-01-20 10:42:58 -08:00
macroid.lean chore: remove unnecessary |s from test 2020-01-25 20:24:22 -08:00
meta1.lean chore: fix tests 2020-01-11 15:20:37 -08:00
meta2.lean fix: checkAssignment was overwriting assignment 2020-02-11 16:11:56 -08:00
meta3.lean chore: fix tests 2020-01-11 15:20:37 -08:00
meta4.lean fix: forallBoundedTelescope 2019-12-11 18:08:41 -08:00
meta5.lean feat: add getParamNames 2020-02-23 12:01:06 -08:00
meta6.lean feat: remove hack 2020-03-06 13:43:19 -08:00
mixedMacroRules.lean feat: allow macro_rules block with different syntax node kinds 2020-01-26 08:39:40 -08:00
natlit.lean fix: nat lit support 2020-03-13 06:54:33 -07:00
nested_match_bug.lean fix(library/equations_compiler): equation compiler bug reported by @dselsam on Zulip 2019-08-12 19:20:26 -07:00
new_compiler.lean fix(tests/lean/run/new_compiler): broken test 2019-08-16 09:46:44 -07:00
new_frontend2.lean feat: declare_syntax_cat without importing Init.Lean 2020-01-11 09:02:50 -08:00
new_inductive.lean chore(frontends/lean): fun x, e ==> fun x => e 2019-07-02 13:22:11 -07:00
new_inductive2.lean chore(tests/lean): fix more tests 2019-03-21 15:11:05 -07:00
newfrontend1.lean refactor: remove support for fun {a : A} => ... 2020-03-26 10:40:16 -07:00
newfrontend2.lean feat: extend scope of cdot notation 2020-01-30 11:42:37 -08:00
newfrontend3.lean feat: propagate expected type at elabFunCore 2020-02-11 17:47:51 -08:00
newfrontend4.lean doc: document why example fails 2020-02-12 13:46:55 -08:00
newfrontend5.lean refactor: remove support for fun {a : A} => ... 2020-03-26 10:40:16 -07:00
noncomputable_bug.lean chore(tests/lean): fix tests 2019-07-08 22:11:19 -07:00
parseCore.lean chore: disable test on windows 2020-02-04 14:21:38 -08:00
patbug.lean fix: to_pattern_fn bug 2020-03-17 12:58:08 -07:00
print_error.lean fix: little details 2020-01-12 08:02:48 -08:00
print_error.lean.expected.out chore: lowercase error messages 2020-01-12 08:21:26 -08:00
ptrAddr.lean chore: fix test 2020-02-15 16:15:37 -08:00
quasi_pattern_unification_approx_issue.lean chore(frontends/lean): fun x, e ==> fun x => e 2019-07-02 13:22:11 -07:00
rc_tests.lean chore: fix tests 2019-11-05 14:44:05 -08:00
recInfo1.lean test: add mkRecursorInfo tests 2020-02-19 19:08:03 -08:00
reduce1.lean feat: allow decide! and nativeDecide! take _ as an argument 2020-03-18 16:00:06 -07:00
reduce2.lean test: add rfl tests 2020-03-17 16:18:18 -07:00
reduce3.lean test: decide! tests 2020-03-18 16:48:28 -07:00
Reid1.lean feat: simplify CoeFun and CoeSort 2020-01-29 21:56:26 -08:00
replace.lean test: add Expr.find? test 2020-02-17 19:49:13 -08:00
revert1.lean feat: add evalRevert 2020-02-08 18:51:11 -08:00
sharecommon.lean chore: rename test 2020-02-28 10:53:41 -08:00
struct_instance_in_eqn.lean chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
structInst.lean feat: elaborate structure instance default values 2020-02-17 20:16:44 -08:00
structInst2.lean test: structure instance tests 2020-02-18 17:50:42 -08:00
structInst3.lean fix: structure instance parser 2020-02-18 10:28:43 -08:00
structInst4.lean fix: structure instance parser 2020-02-18 20:27:04 -08:00
structure.lean feat: add getBaseStructurePath 2019-12-14 13:11:22 -08:00
subst1.lean fix: bug at subst tactic 2020-02-09 19:25:15 -08:00
synth1.lean fix: lambdaMetaTelescope 2019-12-11 17:50:34 -08:00
synthPending1.lean feat: synthPending implementation 2020-03-13 13:52:00 -07:00
tactic.lean chore: fix tests 2019-12-17 07:37:58 -08:00
tacticExtOverlap.lean feat: add evalChoice 2020-02-18 16:31:36 -08:00
task_test.lean test(tests): use #eval and move tests 2019-09-19 14:38:52 -07:00
task_test2.lean test(tests): use #eval and move tests 2019-09-19 14:38:52 -07:00
termElab.lean refactor: remove support for fun {a : A} => ... 2020-03-26 10:40:16 -07:00
termParserAttr.lean refactor: remove ParserKind 2020-01-30 20:56:46 -08:00
termparsertest1.lean test: add parser test at tests/lean/run 2020-01-08 21:09:17 -08:00
test_single.sh chore: fix tests 2019-11-22 07:56:06 -08:00
toExpr.lean feat: add ToExpr instances 2020-03-18 10:22:24 -07:00
trace.lean refactor: MonadTracer and helper functions 2019-12-08 09:05:15 -08:00
type_class_performance1.lean chore(tests/lean): fix more tests 2019-03-21 15:11:05 -07:00
typeclass_append.lean chore: reduce problem size 2020-02-12 21:27:34 -08:00
typeclass_coerce.lean fix: add isNewAnswer predicate 2020-01-09 13:37:21 -08:00
typeclass_diamond.lean feat: improve support for nat literals 2020-01-09 15:36:46 -08:00
typeclass_easy.lean feat: add #synth command to new frontend 2020-01-09 09:54:45 -08:00
typeclass_metas_internal_goals1.lean chore: reactivate typeclass test 2020-01-09 11:46:10 -08:00
typeclass_metas_internal_goals2.lean chore: reactivate typeclass test 2020-01-09 11:46:10 -08:00
typeclass_metas_internal_goals3.lean chore: reactivate typeclass test 2020-01-09 11:46:10 -08:00
typeclass_metas_internal_goals4.lean chore: reactivate typeclass test 2020-01-09 11:46:10 -08:00
typeclass_outparam.lean chore: reactivate typeclass test 2020-01-09 11:47:48 -08:00
ubscalar.lean test(tests/lean/run/ubscalar): save UB scalar field test 2019-07-28 10:11:35 -07:00
unif_issue.lean feat: workaround for the constant approximation issue 2020-03-06 16:47:02 -08:00
unif_issue2.lean feat: workaround for the constant approximation issue 2020-03-06 16:47:02 -08:00
update.lean chore: fix tests 2019-11-17 08:53:18 -08:00