| .. |
|
bind_with_existential_types.lean
|
doc: elabissue for bind with existential types
|
2019-10-21 22:28:14 -07:00 |
|
ImplicitLambdas.lean
|
test: elab feature request: implicit lambda insertion
|
2019-10-08 17:51:45 +02:00 |
|
issues1.lean
|
|
|
|
issues2.lean
|
|
|
|
issues3.lean
|
|
|
|
issues4.lean
|
test: add new elab issue from @joehendrix
|
2019-10-03 17:23:53 -07:00 |
|
issues5.lean
|
tests: add more issues
|
2019-10-15 07:47:09 -07:00 |
|
issues6.lean
|
tests: add more issues
|
2019-10-15 07:47:09 -07:00 |
|
issues7.lean
|
tests: add more issues
|
2019-10-15 07:47:09 -07:00 |
|
issues8.lean
|
test: document another elab issue
|
2019-10-15 09:41:07 -07:00 |
|
let_destruct_inside_forall.lean
|
doc: add comment describing why examples fail
|
2019-10-28 18:06:07 -07:00 |
|
namespace_vs_prefix.lean
|
doc: elabissue for simple namespace issue
|
2019-10-31 21:08:12 -07:00 |
|
overload_with_list_coercion.lean
|
doc: explain why elaborator fails and propose alternative elaboration strategies
|
2019-10-31 08:50:01 -07:00 |
|
ProjNotation.lean
|
doc: elabissue for underapplied proj notation
|
2019-10-28 18:07:22 -07:00 |
|
Reid1.lean
|
test: issue reported by Reid
|
2019-10-19 13:26:47 -07:00 |
|
typeclasses_with_emetavariables.lean
|
doc: elabissues from reid visit
|
2019-10-21 22:27:58 -07:00 |
|
typeclasses_with_preconditions.lean
|
doc: elabissues from reid visit
|
2019-10-21 22:27:58 -07:00 |
|
typeclasses_with_umetavariables.lean
|
doc: elabissues from reid visit
|
2019-10-21 22:27:58 -07:00 |
|
variable_universe_bug.lean
|
doc: elabissue for variable universe bug
|
2019-10-28 17:59:23 -07:00 |