sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
lean4/tests/elabissues
History
Joe Hendrix 1118931516 feat: add bitwise operations to reduceNat? and kernel (#3134) 
This adds bitwise operations to reduceNat? and the kernel. It
incorporates some basic test cases to validate the correct operations
are associated.
2024-01-11 18:12:45 +00:00
..
anonymous_constructor_error_msg.lean
doc: document issue
2020-02-18 10:41:12 -08:00
bind_with_existential_types.lean
chore: avoid Has prefix in type classes
2020-10-27 18:29:19 -07:00
equation_compiler_slow_with_many_constructors2.lean
chore: avoid Has prefix in type classes
2020-10-27 18:29:19 -07:00
equation_compiler_slow_with_many_constructors.lean
doc: add workarounds, and describe what we need in the new equation compiler
2020-02-05 11:46:35 -08:00
error_aux_decl_exists.lean
doc: document issue
2020-02-18 10:52:12 -08:00
ImplicitLambdas.lean
test: elab feature request: implicit lambda insertion
2019-10-08 17:51:45 +02:00
invalid_field_notation_error_msg.lean
chore: fix more typos in comments
2023-10-08 14:37:34 -07:00
issues1.lean
chore: update
2019-11-02 12:12:27 -07:00
issues2.lean
test(elabissues): document some of the known problems
2019-09-21 10:17:26 -07:00
issues3.lean
chore: avoid Has prefix in type classes
2020-10-27 18:29:19 -07:00
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
fix: malformed/misaligned markdown code fences
2022-07-20 11:12:42 +02:00
leaky_tmp_metavars2.lean
doc: tc triggers nested tc, potentially with tmp metavar leak
2019-11-06 10:15:05 -08:00
leaky_tmp_metavars.lean
chore: fix more typos in comments
2023-10-08 14:37:34 -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
nested_namespace_vs_prefix.lean
doc: namespace A.B vs namespace A namespace B
2019-11-06 10:16:33 -08:00
overload_with_list_coercion.lean
doc: explain why elaborator fails and propose alternative elaboration strategies
2019-10-31 08:50:01 -07:00
patternIssue.lean
test: pattern confusion example
2019-12-19 13:36:22 -08:00
private.lean
doc: document private keyword elaboration issues
2019-12-05 08:55:21 -08:00
ProjNotation.lean
doc: elabissue for underapplied proj notation
2019-10-28 18:07:22 -07:00
reduceNatWithMeta.lean
feat: add bitwise operations to reduceNat? and kernel (#3134)
2024-01-11 18:12:45 +00:00
Reid1.lean
test: issue reported by Reid
2019-10-19 13:26:47 -07:00
structInst.lean
chore: avoid Has prefix in type classes
2020-10-27 18:29:19 -07:00
structure_same_names2.lean
doc: elabissue for structure same-name error msg
2020-02-18 10:52:44 -08:00
typeclass_nested_validate.lean
chore: disable tests for type class resolution prototype
2019-12-03 14:50:14 -08:00
typeclass_triggers_typeclass.lean
doc: tc triggers nested tc, potentially with tmp metavar leak
2019-11-06 10:15:05 -08:00
typeclasses_with_emetavariables.lean
doc: elabissues from reid visit
2019-10-21 22:27:58 -07:00
typeclasses_with_preconditions.lean
chore: style use · instead of . for lambda dot notation
2022-03-11 07:49:03 -08:00
typeclasses_with_umetavariables.lean
chore: fix more typos in comments
2023-10-08 14:37:34 -07:00
variable_universe_bug.lean
feat: subsume variables under variable
2021-01-22 14:36:05 +01:00
vars.lean
chore: fix more typos in comments
2023-10-08 14:37:34 -07:00
zmod.lean
chore: move pp_options.cpp to Lean
2021-01-27 14:16:12 +01:00