max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean
History
Leonardo de Moura a4d41beab1
perf: match_expr join points (#3580) 
We use `let_delayed` to elaborate `match_expr` join points, which
elaborate the body of the `let` before its value. Thus, there is a
difference between:
- `let_delayed f (x : Expr) := <val>; <body>`
- `let_delayed f := fun (x : Expr) => <val>; <body>`

In the latter, when `<body>` is elaborated, the elaborator does not know
that `f` takes an argument of type `Expr`, and that `f` is a function.
Before this commit ensures the former representation is used.
2024-03-03 18:15:49 +00:00
..
Compiler fix: regression on match expressions with builtin literals (#3521) 2024-02-27 18:49:44 +00:00
Data refactor: simplify some nomatch with nofun (#3564) 2024-03-02 20:43:31 +00:00
Elab perf: match_expr join points (#3580) 2024-03-03 18:15:49 +00:00
Linter chore: add missing copyright headers (#3411) 2024-02-20 01:49:55 +00:00
Meta fix: generalize excessive resource usage (#3575) 2024-03-03 17:58:11 +00:00
Parser fix: missing atomic at match_expr parser (#3572) 2024-03-02 21:55:07 +00:00
ParserCompiler perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
PrettyPrinter fix: make omission syntax be a builtin syntax (part 2) 2024-02-28 09:23:17 +01:00
Server fix: load references asynchronously (#3552) 2024-03-01 13:57:52 +00:00
Util fix: regression on match expressions with builtin literals (#3521) 2024-02-27 18:49:44 +00:00
Widget fix: register builtin rpc methods (#3512) 2024-02-27 00:15:21 +00:00
Attributes.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
AuxRecursor.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Class.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Compiler.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
CoreM.lean fix: broken trace tree on elab runtime exception (#3371) 2024-02-19 11:15:23 +00:00
Data.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Declaration.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
DeclarationRange.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
DocString.lean chore: upstream solve_by_elim (#3408) 2024-02-21 01:16:04 +00:00
Elab.lean feat: macro expander for match_expr terms 2024-03-01 22:33:14 -08:00
Environment.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Eval.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Exception.lean doc: fix typos (#3543) 2024-02-29 13:23:19 +00:00
Expr.lean chore: use let_expr to cleanup code 2024-03-02 10:07:15 -08:00
HeadIndex.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Hygiene.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ImportingFlag.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
InternalExceptionId.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
KeyedDeclsAttribute.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LabelAttribute.lean fix: address symm and label bugs from #3408 (#3429) 2024-02-21 07:21:07 +00:00
LazyInitExtension.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Level.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Linter.lean chore: add missing copyright headers (#3411) 2024-02-20 01:49:55 +00:00
LoadDynlib.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LocalContext.lean chore: upstream omega (#3367) 2024-02-19 00:19:55 +00:00
Log.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Message.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Meta.lean feat: add helper functions for recognizing builtin literals 2024-02-24 16:08:07 -08:00
MetavarContext.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Modifiers.lean fix: auto-completion bugs and performance (#3460) 2024-02-26 09:43:19 +00:00
MonadEnv.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Parser.lean feat: custom error recovery in parser (#3413) 2024-02-21 14:29:54 +00:00
ParserCompiler.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
PrettyPrinter.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ProjFns.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ReducibilityAttrs.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Replay.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ResolveName.lean fix: allow users to disable builtin simprocs in simp args (#3441) 2024-02-21 20:01:11 +00:00
Runtime.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ScopedEnvExtension.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Server.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Structure.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SubExpr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Syntax.lean refactor: simplify some nomatch with nofun (#3564) 2024-03-02 20:43:31 +00:00
ToExpr.lean fix: ToExpr instance for Fin 2024-02-24 16:08:07 -08:00
Util.lean chore: upstream exact? and apply? from Std (#3447) 2024-02-23 21:55:24 +00:00
Widget.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00