max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta
History
Kyle Miller a2226a43ac
feat: encode let_fun using a letFun function (#2973) 
Switches from encoding `let_fun` using an annotated `(fun x : t => b) v`
expression to a function application `letFun v (fun x : t => b)`.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2023-12-18 09:01:42 +00:00
..
Match refactor: CasesOnApp.refineThrough can return a lambda, not an open term (#2974) 2023-11-29 15:58:03 +00:00
Tactic feat: encode let_fun using a letFun function (#2973) 2023-12-18 09:01:42 +00:00
AbstractMVars.lean chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
AbstractNestedProofs.lean chore: do not abstract nested proofs in a proof 2023-11-07 06:23:45 -08:00
ACLt.lean refactor: add configuration options to control WHNF 2023-10-25 03:12:35 -07:00
AppBuilder.lean feat: encode let_fun using a letFun function (#2973) 2023-12-18 09:01:42 +00:00
Basic.lean refactor: add configuration options to control WHNF 2023-10-25 03:12:35 -07:00
CasesOn.lean refactor: CasesOnApp.refineThrough can return a lambda, not an open term (#2974) 2023-11-29 15:58:03 +00:00
Check.lean feat: add implementation-detail hypotheses 2022-10-11 17:24:35 -07:00
Closure.lean fix: use mkAuxTheoremFor when creating helper proof_n theorems 2023-06-21 20:28:17 -07:00
Coe.lean fix: allow function coercion to assign universe mvars 2023-03-08 15:54:07 -08:00
CollectFVars.lean chore: cleanup 2022-07-25 22:39:56 -07:00
CollectMVars.lean doc: fix typos (#2996) 2023-11-30 10:16:33 +00:00
CongrTheorems.lean fix: fixes #1808 2022-11-28 07:48:54 -08:00
Constructions.lean fix: catch kernel exceptions in Kernel.{isDefEq, whnf} 2022-10-20 05:38:29 -07:00
DecLevel.lean refactor: add doc strings, cleanup, and dotted notation friendly API 2022-07-27 16:01:15 -07:00
DiscrTree.lean doc: fix typos (#2915) 2023-11-19 20:00:47 +00:00
DiscrTreeTypes.lean doc: fix typos (#2915) 2023-11-19 20:00:47 +00:00
Eqns.lean chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
Eval.lean fix: fixes #1576 2022-09-09 14:29:48 -07:00
ExprDefEq.lean feat: encode let_fun using a letFun function (#2973) 2023-12-18 09:01:42 +00:00
ExprLens.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
ExprTraverse.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
ForEachExpr.lean feat: abstract visitLet, visitLambda, visitForall 2022-08-25 19:09:16 -07:00
FunInfo.lean feat: add higherOrderOutParam to ParamInfo 2022-07-11 18:52:01 -07:00
GeneralizeTelescope.lean refactor: improve FVarId method discoverability 2022-07-25 22:18:58 -07:00
GeneralizeVars.lean refactor: improve FVarId method discoverability 2022-07-25 22:18:58 -07:00
GetUnfoldableConst.lean doc: improve doc-string for Meta.getConst? 2023-08-24 07:42:28 -07:00
GlobalInstances.lean feat: automatic extension names 2022-10-06 17:19:30 -07:00
IndPredBelow.lean fix: missing whnf in mkBelowBinder and mkMotiveBinder (#2991) 2023-12-01 14:46:09 +00:00
Inductive.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
InferType.lean perf: improve isTypeFormerType 2022-08-19 18:23:28 -07:00
Injective.lean feat: trace nodes for SizeOf and injectivity theorem generation 2023-06-27 16:17:46 -07:00
Instances.lean refactor: add configuration options to control WHNF 2023-10-25 03:12:35 -07:00
KAbstract.lean feat: allow configuring occs in rw 2023-09-13 12:03:18 -07:00
KExprMap.lean chore: fix typos in comments 2023-10-08 10:46:05 +02:00
LevelDefEq.lean refactor: replace ignoreLevelMVarDepth by levelAssignDepth 2022-12-19 20:14:17 +01:00
Match.lean
MatchUtil.lean doc: apply suggestions from code review 2022-07-20 15:30:30 -07:00
Offset.lean chore: fix typos in comments 2023-10-08 10:46:05 +02:00
PPGoal.lean chore: fix typos in comments 2023-10-08 10:46:05 +02:00
RecursorInfo.lean chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
Reduce.lean chore: use a[i]! for array accesses that may panic 2022-07-02 15:12:05 -07:00
ReduceEval.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
SizeOf.lean feat: trace nodes for SizeOf and injectivity theorem generation 2023-06-27 16:17:46 -07:00
Structure.lean
SynthInstance.lean fix: fixes #2775 2023-11-03 05:56:59 -07:00
Tactic.lean feat: add congr tactic 2022-08-01 18:44:07 -07:00
Transform.lean fix: PackMutual: Eta-Expand as needed (#2902) 2023-11-22 14:25:56 +00:00
TransparencyMode.lean
UnificationHint.lean chore: fix configuration for UnificationHints 2023-10-25 03:12:35 -07:00
WHNF.lean feat: encode let_fun using a letFun function (#2973) 2023-12-18 09:01:42 +00:00