Leonardo de Moura c55376a1ba chore: more conventional MonadIO		2020-08-20 11:13:10 -07:00
..
EqnCompiler	refactor: DepElim.lean ==> Match.lean	2020-08-17 16:34:39 -07:00
Tactic	chore: preparing to refactor DepElim	2020-08-14 19:02:20 -07:00
AbstractMVars.lean	chore: move HashMap and HashSet to Std	2020-06-25 12:46:56 -07:00
AppBuilder.lean	feat: add mkLt and mkLe	2020-08-07 14:47:11 -07:00
Basic.lean	feat: instantiate metavariables in LocalDecls	2020-08-14 19:02:38 -07:00
Check.lean
DiscrTree.lean
DiscrTreeTypes.lean	chore: move PersistentHashMap and PersistentHashSet to Std	2020-06-25 11:56:00 -07:00
EqnCompiler.lean	refactor: DepElim.lean ==> Match.lean	2020-08-17 16:34:39 -07:00
Exception.lean	feat: add (ref : Syntax) to Meta.Exception.tactic	2020-08-06 10:14:32 -07:00
ExprDefEq.lean	fix: isDefEqQuick	2020-08-15 13:24:43 -07:00
FunInfo.lean
GeneralizeTelescope.lean
InferType.lean	feat: inductive datatype header validation	2020-07-09 15:34:25 -07:00
Instances.lean	chore: more conventional MonadIO	2020-08-20 11:13:10 -07:00
KAbstract.lean
LevelDefEq.lean	feat: add commitWhenSome?	2020-08-16 10:55:15 -07:00
Message.lean	feat: add (ref : Syntax) to Meta.Exception.tactic	2020-08-06 10:14:32 -07:00
Offset.lean
RecursorInfo.lean	chore: more conventional MonadIO	2020-08-20 11:13:10 -07:00
Reduce.lean
ReduceEval.lean	feat: add (ref : Syntax) to Meta.Exception.other	2020-08-06 09:40:16 -07:00
SynthInstance.lean	feat: add (ref : Syntax) to Meta.Exception.other	2020-08-06 09:40:16 -07:00
Tactic.lean
WHNF.lean	feat: add throwOther	2020-07-31 14:34:51 -07:00