lean4-htt/src/Lean
Leonardo de Moura ff0f3bfc61 fix: interaction between overloaded notation and delayed coercions
The new test exposes this issue.
2022-03-06 09:49:15 -08:00
..
Compiler chore: workaround for compiler closed term extraction issue 2022-03-01 09:01:08 -08:00
Data fix: PrefixTree WellFormed type 2022-03-06 07:30:34 -08:00
Elab fix: interaction between overloaded notation and delayed coercions 2022-03-06 09:49:15 -08:00
Meta fix: a match application is stuck if one of the discriminants contain metavariables 2022-03-06 07:51:09 -08:00
Parser chore: add auxiliary notation for ForIn' 2022-03-03 19:10:24 -08:00
ParserCompiler
PrettyPrinter feat: delaborate cond using bif-then-else 2022-03-03 07:41:39 -08:00
Server feat: propagate actual file name in file worker 2022-02-27 10:33:27 +01:00
Util fix: trace_state messages should not be lost during backtracking 2022-02-28 11:07:41 -08:00
Widget chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
Attributes.lean chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
AuxRecursor.lean feat: add isBRecOnRecursor 2022-02-23 13:09:29 -08:00
Class.lean
Compiler.lean feat: add isNoncomputable function for querying whether a given declaration has been marked as "noncomputable" by users 2022-02-16 13:20:31 -08:00
CoreM.lean chore: increase maxHeartbeats default values 2022-02-28 15:44:08 -08:00
Data.lean
Declaration.lean feat: improve getCompletionKindForDecl 2021-12-15 12:57:09 -08:00
DeclarationRange.lean feat: record declaration ranges of builtin parsers & elaborators 2021-11-26 17:13:19 +01:00
DocString.lean feat: add position to mod doc 2022-02-16 13:50:19 -08:00
Elab.lean feat: save syntax around recursive applications 2021-12-16 17:13:55 -08:00
Environment.lean fix: use private names for theorems that are created on demand 2022-02-07 13:16:22 -08:00
Eval.lean feat: use BaseIO more in Init.System.IO 2021-12-14 09:33:52 +01:00
Exception.lean chore: cleanup 2022-01-26 09:18:17 -08:00
Expr.lean feat: improve delta? method 2022-02-09 13:31:55 -08:00
HeadIndex.lean chore: cleanup 2022-01-26 09:18:17 -08:00
Hygiene.lean chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
ImportingFlag.lean chore: clarify safety of compile-time code execution 2022-01-20 18:55:57 +01:00
InternalExceptionId.lean chore: cleanup 2022-01-26 09:18:17 -08:00
KeyedDeclsAttribute.lean chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
LazyInitExtension.lean chore: remove arbitrary 2022-01-15 12:14:27 -08:00
Level.lean chore: cleanup 2022-01-26 09:18:17 -08:00
LoadDynlib.lean feat: expose --load-dynlib functionality to Lean code 2021-12-15 08:26:48 +00:00
LocalContext.lean chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
Message.lean feat: improve split tactic error message 2022-02-23 16:00:42 -08:00
Meta.lean refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files 2021-12-06 09:57:00 -08:00
MetavarContext.lean fix: incorrect dependencies due to assigned variables 2022-02-15 12:15:45 -08:00
Modifiers.lean
MonadEnv.lean feat: include types in the "ambiguous, possible interpretations" error message 2022-03-06 07:26:31 -08:00
Parser.lean
ParserCompiler.lean chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
PrettyPrinter.lean chore: cleanup 2022-01-26 09:18:17 -08:00
ProjFns.lean
ReducibilityAttrs.lean chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
ResolveName.lean fix: completion for aliases 2021-12-10 12:14:11 -08:00
Runtime.lean
ScopedEnvExtension.lean chore: remove arbitrary 2022-01-15 12:14:27 -08:00
Server.lean
Structure.lean chore: remove arbitrary 2022-01-15 12:14:27 -08:00
Syntax.lean chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
ToExpr.lean
Util.lean fix: igore instance implicit arguments in term ordering used at simp 2022-01-24 18:57:31 -08:00
Widget.lean