| .. |
|
EqnCompiler
|
refactor: cleanup
|
2020-08-24 17:47:27 -07:00 |
|
Tactic
|
chore: remove workaround
|
2020-08-26 16:24:20 -07:00 |
|
AbstractMVars.lean
|
refactor: build all main monads on top of ECoreM
|
2020-08-20 18:36:04 -07:00 |
|
AppBuilder.lean
|
chore: remove workaround
|
2020-08-26 16:24:20 -07:00 |
|
Basic.lean
|
fix: collect metavars occurring in delayed assignments
|
2020-08-27 14:59:54 -07:00 |
|
Check.lean
|
refactor: add MonadMetaM class
|
2020-08-24 12:17:47 -07:00 |
|
CollectMVars.lean
|
fix: collect metavars occurring in delayed assignments
|
2020-08-27 14:59:54 -07:00 |
|
DiscrTree.lean
|
chore: remove prelude commands from Lean package
|
2020-06-25 11:21:17 -07:00 |
|
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: uniform Exceptions
|
2020-08-21 17:02:21 -07:00 |
|
ExprDefEq.lean
|
refactor: add MonadMetaM class
|
2020-08-24 12:17:47 -07:00 |
|
FunInfo.lean
|
chore: remove prelude commands from Lean package
|
2020-06-25 11:21:17 -07:00 |
|
GeneralizeTelescope.lean
|
refactor: cleanup
|
2020-08-24 17:47:27 -07:00 |
|
InferType.lean
|
refactor: move polymorphic Meta methods back to Meta namespace
|
2020-08-25 14:57:58 -07:00 |
|
Instances.lean
|
refactor: polymorphic applyAttributes
|
2020-08-27 10:46:33 -07:00 |
|
KAbstract.lean
|
refactor: use MonadControlT
|
2020-08-25 13:54:42 -07:00 |
|
LevelDefEq.lean
|
refactor: move polymorphic Meta methods back to Meta namespace
|
2020-08-25 14:57:58 -07:00 |
|
Offset.lean
|
refactor: add MonadMetaM class
|
2020-08-24 12:17:47 -07:00 |
|
RecursorInfo.lean
|
feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions
|
2020-08-22 16:00:43 -07:00 |
|
Reduce.lean
|
refactor: add MonadMetaM class
|
2020-08-24 12:17:47 -07:00 |
|
ReduceEval.lean
|
refactor: build all main monads on top of ECoreM
|
2020-08-20 18:36:04 -07:00 |
|
SynthInstance.lean
|
refactor: move polymorphic Meta methods back to Meta namespace
|
2020-08-25 14:57:58 -07:00 |
|
Tactic.lean
|
chore: remove prelude commands from Lean package
|
2020-06-25 11:21:17 -07:00 |
|
TransparencyMode.lean
|
refactor: move TransparencyMode to its own file
|
2020-08-24 12:17:47 -07:00 |
|
WHNF.lean
|
refactor: move polymorphic Meta methods back to Meta namespace
|
2020-08-25 14:57:58 -07:00 |
