max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Elab
History
Leonardo de Moura 06a767089c fix: do not use `mkAppM id #[e]`` 
If `e` has type `forall {A : Type}, B`, ``mkAppM `id #[e]`` fails
since it will try to synthesize the implicit argument `A : Type`.
We can avoid this issue by using
1- ``mkAppOptM `id #[none, some e]``, or
2- `mkId e`
2020-07-27 15:24:06 -07:00
..
Tactic chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Alias.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
App.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Binders.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
BuiltinNotation.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
CollectFVars.lean feat: add Lean.Elab.CollectFVars 2020-07-15 16:32:22 -07:00
Command.lean fix: track NameGenerator at CommandElabM 2020-07-27 14:31:43 -07:00
Declaration.lean feat: add expandFields 2020-07-17 11:10:34 -07:00
DeclModifiers.lean chore: add mkAuxDefinition 2020-07-24 10:45:32 -07:00
DeclUtil.lean fix: missing file 2020-07-17 17:25:15 -07:00
Definition.lean feat: remove unused variables 2020-07-15 16:32:22 -07:00
DoNotation.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Exception.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Frontend.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Import.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Inductive.lean feat: structure resulting universe 2020-07-22 14:52:23 -07:00
Level.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Log.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Match.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Quotation.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
ResolveName.lean fix: resolveGlobalName for atomic references to private names 2020-07-23 14:58:19 -07:00
StrategyAttrs.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
StructInst.lean fix: do not assume the prefix of a projection function name is the structure name 2020-07-16 11:10:20 -07:00
Structure.lean fix: do not use `mkAppM id #[e]`` 2020-07-27 15:24:06 -07:00
Syntax.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
SyntheticMVars.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Tactic.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Term.lean feat: zeta-expand auxiliary let-declarations and mark to_default as reducible 2020-07-24 11:51:50 -07:00
Util.lean chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00