Leonardo de Moura 2254da0367 test: add simple test		2019-12-03 10:42:43 -08:00
..
Compiler
Elaborator
EqnCompiler
Meta	test: add simple test	2019-12-03 10:42:43 -08:00
Parser
TypeClass
Attributes.lean
AuxRecursor.lean
Class.lean	feat: add checkOutParam validation	2019-12-01 18:32:48 -08:00
Compiler.lean
Declaration.lean
Elaborator.lean
Environment.lean
EqnCompiler.lean
Expr.lean	feat: add etaExpandedStrict?	2019-12-03 10:30:19 -08:00
Format.lean
KVMap.lean
LBool.lean
Level.lean	refactor: Level.instantiate ==> Level.instantiateParams	2019-12-01 18:32:48 -08:00
Linter.lean
LocalContext.lean	chore: add abbreviations MVarId and FVarId	2019-11-28 08:18:06 -08:00
LOption.lean	feat: add trySynthInstance	2019-12-01 18:52:31 -08:00
Message.lean
Meta.lean	feat: add SynthInstance.lean	2019-12-01 18:32:48 -08:00
MetavarContext.lean	feat: add withMVarContext	2019-12-02 10:50:00 -08:00
Modifiers.lean
MonadCache.lean
Name.lean	fix: abstractMVars	2019-11-27 10:53:25 -08:00
NameGenerator.lean
Options.lean
Parser.lean
Path.lean
Position.lean	chore: remove DecidableEq workaround	2019-11-26 17:30:18 -08:00
ProjFns.lean
ReducibilityAttrs.lean
Runtime.lean
Scopes.lean
SMap.lean
Syntax.lean
ToExpr.lean
Trace.lean	feat: ensure trace messages at MetaM save Environment, MetavarContext, and LocalContext	2019-11-22 11:50:19 -08:00
TypeClass.lean
Util.lean
WHNF.lean	chore: add abbreviations MVarId and FVarId	2019-11-28 08:18:06 -08:00