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 7b84b4cdaa fix: improve inductive indices elaboration 
TODO: convert fixed indices to parameters. Motivation: types such as
```lean
inductive Foo : List α → Type
  | mk : Foo []
```
Users should not need to write
```lean
inductive Foo {α} : List α → Type
  | mk : Foo []
```
2022-03-08 17:48:46 -08:00
..
Compiler chore: workaround for compiler closed term extraction issue 2022-03-01 09:01:08 -08:00
Data feat: LSP code folding support 2022-03-07 17:23:35 +01:00
Elab fix: improve inductive indices elaboration 2022-03-08 17:48:46 -08:00
Meta chore: link orphan file 2022-03-07 10:59:49 +01: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 chore: Clean up LSP folding a little 2022-03-07 17:23:35 +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 refactor: avoid Name, MVarId, and FVarId confusion 2021-09-07 19:06:50 -07:00
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 feat: add Lean.Rat for implementing decision procedures 2021-09-14 19:18:12 -07:00
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 feat: private fields 2021-08-02 20:20:21 -07:00
MonadEnv.lean feat: include types in the "ambiguous, possible interpretations" error message 2022-03-06 07:26:31 -08:00
Parser.lean feat: scientific parser alias for scientificLit 2022-03-08 18:54:05 +01:00
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 chore: naming convention and cleanup 2021-08-05 16:23:21 -07:00
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 refactor: shuffle classes to avoid dependency loops 2021-08-01 09:58:44 +02:00
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 chore: remove ToExpr Expr 2021-08-14 06:16:46 -07:00
Util.lean fix: igore instance implicit arguments in term ordering used at simp 2022-01-24 18:57:31 -08:00
Widget.lean refactor: consistent naming of widget modules 2021-08-24 08:57:41 -07:00