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

chore: add isDefEq abbreviation for isExprDefEq

Browse source 
Most tactic users will never use `isLevelDefEq`.
This commit is contained in:
Leonardo de Moura 2019-11-22 11:54:06 -08:00
parent 7306343589
commit ea2d971bd3
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Meta/ExprDefEq.lean
View file

@ -999,5 +999,7 @@ partial def isExprDefEqAuxImpl : Expr → Expr → MetaM Bool
@[init] def setIsExprDefEqAuxRef : IO Unit :=
isExprDefEqAuxRef.set isExprDefEqAuxImpl
abbrev isDefEq := @isExprDefEq
end Meta
end Lean

4
tests/lean/run/meta2.lean
View file

@ -177,8 +177,8 @@ do print "----- tst6 -----";
m2 ← mkFreshExprMVar type;
let t := mkApp io x;
-- we need to use foApprox to solve `?m1 ?m2 =?= IO x`
check $ not <$> isExprDefEq (mkApp m1 m2) t;
check $ approxDefEq $ isExprDefEq (mkApp m1 m2) t;
check $ not <$> isDefEq (mkApp m1 m2) t;
check $ approxDefEq $ isDefEq (mkApp m1 m2) t;
v ← getAssignment m1;
check $ pure $ v == io;
v ← getAssignment m2;