lean4-htt/src/Lean
Leonardo de Moura 0717bdb66d fix: fixes #1419
2022-08-04 15:44:38 -07:00
..
Compiler feat: add go-to-def for simple attributes 2022-07-31 16:36:54 +02:00
Data feat: add missingDocs linter 2022-07-31 18:18:21 -07:00
Elab chore: improve expandParen do notation 2022-08-04 10:01:32 -07:00
Linter fix: unused variables in foreign definition 2022-08-03 18:15:15 -07:00
Meta fix: fixes #1419 2022-08-04 15:44:38 -07:00
Parser chore: use Category declarations for builtin cats too (#1400) 2022-08-03 18:10:54 -07:00
ParserCompiler
PrettyPrinter refactor: improve FVarId method discoverability 2022-07-25 22:18:58 -07:00
Server fix: do not show inaccessible variable in hover 2022-08-04 11:28:46 -07:00
Util chore: cleanup 2022-07-25 22:39:56 -07:00
Widget feat: add option pp.showLetValues 2022-07-26 17:53:34 -07:00
Attributes.lean feat: add go-to-def for simple attributes 2022-07-31 16:36:54 +02:00
AuxRecursor.lean feat: add [elabAsElim] elaboration strategy 2022-07-28 20:08:29 -07:00
Class.lean chore: enforce naming convention 2022-08-01 09:58:11 -07:00
Compiler.lean
CoreM.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
Data.lean
Declaration.lean chore: remove unnecessary french quotes 2022-07-29 20:53:01 -07:00
DeclarationRange.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
Deprecated.lean feat: add [deprecated] attribute 2022-07-24 18:06:03 -07:00
DocString.lean fix: findDocString? 2022-08-04 10:32:41 -07:00
Elab.lean refactor: add Elab/Calc.lean 2022-07-24 13:30:05 -07:00
Environment.lean doc: add some doc strings at Environment.lean 2022-07-30 15:05:13 -07:00
Eval.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
Exception.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
Expr.lean chore: remove redundant data form Expr.Data 2022-07-29 21:25:03 -07:00
HeadIndex.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
Hygiene.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
ImportingFlag.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
InternalExceptionId.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
KeyedDeclsAttribute.lean feat: add go-to-def for simple attributes 2022-07-31 16:36:54 +02:00
LazyInitExtension.lean
Level.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
Linter.lean feat: add missingDocs linter 2022-07-31 18:18:21 -07:00
LoadDynlib.lean feat: replace constant with opaque 2022-06-14 17:02:59 -07:00
LocalContext.lean feat: add LocalContext.replaceFVarId 2022-08-03 11:21:55 -07:00
Log.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
Message.lean chore: style 2022-07-29 12:27:01 -07:00
Meta.lean feat: add evalTerm and Meta.evalExpr 2022-06-28 19:14:40 -07:00
MetavarContext.lean chore: style 2022-07-30 21:29:12 -07:00
Modifiers.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
MonadEnv.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
Parser.lean fix: bound syntax kind at v:(ppSpace ident) etc. 2022-07-07 11:49:35 +02:00
ParserCompiler.lean chore: use a[i]! for array accesses that may panic 2022-07-02 15:12:05 -07:00
PrettyPrinter.lean feat: ppCategory 2022-07-15 10:58:29 +02:00
ProjFns.lean chore: doc strings for ProjFns.lean 2022-08-02 15:58:56 -07:00
ReducibilityAttrs.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
ResolveName.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
Runtime.lean feat: replace constant with opaque 2022-06-14 17:02:59 -07:00
ScopedEnvExtension.lean chore: remove unnecessary french quotes 2022-07-29 20:53:01 -07:00
Server.lean
Structure.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
SubExpr.lean refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
Syntax.lean chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
ToExpr.lean doc: some doc strings 2022-07-30 21:18:50 -07:00
Util.lean feat: add HasConstCache 2022-03-15 08:39:48 -07:00
Widget.lean feat: user widgets 2022-07-25 08:01:27 -07:00