max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add tryOpt

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-01 12:46:34 -08:00
parent 00b991baf6
commit 2867cd627b
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Init/Lean/Meta/LevelDefEq.lean
View file

@ -163,6 +163,22 @@ do s ← get;
(do restore env mctx postponed; pure false))
(fun ex => do restore env mctx postponed; throw ex)
@[specialize] def tryOpt {α} (x : MetaM (Option α)) : MetaM (Option α) :=
do s ← get;
let env := s.env;
let mctx := s.mctx;
let postponed := s.postponed;
modify $ fun s => { postponed := {}, .. s };
catch
(do a? ← x;
match a? with
| some a =>
condM processPostponed
(pure (some a))
(do restore env mctx postponed; pure none)
| none => do restore env mctx postponed; pure none)
(fun ex => do restore env mctx postponed; throw ex)
/- Public interface -/
def isLevelDefEq (u v : Level) : MetaM Bool :=