Leonardo de Moura 2694e7798a refactor: add MonadBacktrack ... The new class specifies an interface for saving and restoring the backtrackable part of the state. This commit also fixes a few issues. - `commitWhen` at `LevelDefEq` was defining a checkpoint for the `isDefEq` methods, and it affects how postponed universe constraints are handled. However, the name suggests it is similar to `commitWhenSome?`, and consequently it was used in other places that had nothing to do with `isDefEq`. So, I renamed it, and provided the generic `commitWhen` at the new `MonadBacktrack.lean` file. - We were restoring more state then needed in a few places. For example, we were discarding all caches. - At `SyntheticMVars.lean`, we were using the `Meta.commitWhenSome?` method which does not restore the `Term.State`.		2021-04-11 19:10:41 -07:00
..
Match	feat: try to improve dependent pattern matching failure error message	2021-03-30 23:40:11 -07:00
Tactic	chore: rename option hygienicIntro ==> tactic.hygienic	2021-04-10 16:09:04 -07:00
AbstractMVars.lean	chore: use deriving BEq	2020-12-22 18:10:20 -08:00
AbstractNestedProofs.lean	chore: change checkCache type	2020-12-06 16:24:51 -08:00
AppBuilder.lean	chore: improve congrDefault	2021-03-16 15:59:11 -07:00
Basic.lean	refactor: add MonadBacktrack	2021-04-11 19:10:41 -07:00
Check.lean	chore: throwError! => throwError, throwErrorAt! => throwErrorAt	2021-03-11 11:59:45 -08:00
Closure.lean	chore: trace[...]! ==> trace[...]	2021-03-10 18:44:43 -08:00
Coe.lean	feat: unfold coercions and coeFun, coeSort, coeM, liftCoeM	2021-02-14 10:27:34 -08:00
CollectFVars.lean	refactor: move collectFVars to Meta	2021-03-26 19:16:21 -07:00
CollectMVars.lean	chore: remove "liftable methods"	2020-12-09 15:06:07 -08:00
DiscrTree.lean	fix: non-dependent arrow vs dependent arrow issue at DiscrTree	2021-03-25 13:04:24 -07:00
DiscrTreeTypes.lean	feat: add support for "arrow" at DiscrTree	2021-03-25 12:21:10 -07:00
ExprDefEq.lean	refactor: add MonadBacktrack	2021-04-11 19:10:41 -07:00
ForEachExpr.lean	chore: remove unnecessary do	2021-01-26 12:41:07 -08:00
FunInfo.lean	fix: typo at ParamInfo.isExplicit	2021-01-11 07:08:17 -08:00
GeneralizeTelescope.lean	chore: throwError! => throwError, throwErrorAt! => throwErrorAt	2021-03-11 11:59:45 -08:00
GetConst.lean	feat: add TransparencyMode.instances	2020-11-29 18:12:33 -08:00
Inductive.lean	feat: add deriving DecidableEq	2020-12-17 17:30:23 -08:00
InferType.lean	fix: do not try to pretty-print unknown metavariables	2021-04-08 18:16:05 +02:00
Instances.lean	feat: mkConstWithLevelParams	2021-03-20 08:28:18 -07:00
KAbstract.lean	chore: cleanup	2021-01-05 14:58:23 -08:00
LevelDefEq.lean	refactor: add MonadBacktrack	2021-04-11 19:10:41 -07:00
Match.lean	chore: remove #lang lean4 header	2020-10-25 09:54:07 -07:00
MatchUtil.lean	feat: add contradiction	2021-03-03 17:00:54 -08:00
Offset.lean	fix: bug at isDefEqOffset	2021-03-02 17:28:40 -08:00
PPGoal.lean	feat: set pp.inaccessibleNames true when visualizing tactic state	2021-03-21 18:21:46 -07:00
RecursorInfo.lean	chore: throwError! => throwError, throwErrorAt! => throwErrorAt	2021-03-11 11:59:45 -08:00
Reduce.lean	chore: add cache	2021-01-06 06:21:55 -08:00
ReduceEval.lean	chore: throwError! => throwError, throwErrorAt! => throwErrorAt	2021-03-11 11:59:45 -08:00
SizeOf.lean	chore: convert keywords to snake_case	2021-03-12 13:34:51 -08:00
SortLocalDecls.lean	fix: perform topological sort on pattern variables	2021-03-22 20:35:07 -07:00
SynthInstance.lean	chore: throwError! => throwError, throwErrorAt! => throwErrorAt	2021-03-11 11:59:45 -08:00
Tactic.lean	feat: add AuxLemma.lean	2021-03-09 18:25:19 -08:00
Transform.lean	fix: make Meta.transform use matching aux functions	2021-01-17 10:04:33 +01:00
TransparencyMode.lean	chore: add Repr instance for TransparencyMode	2021-02-04 20:40:05 -08:00
UnificationHint.lean	refactor: add MonadBacktrack	2021-04-11 19:10:41 -07:00
WHNF.lean	chore: remove when and «unless»	2021-03-20 18:52:18 -07:00