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

feat: add mkLt and mkLe

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-07 14:46:11 -07:00
parent 3b0ec1b20a
commit 6b18f486d1
2 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Meta/AppBuilder.lean
View file

@ -352,5 +352,13 @@ h ← mkEqRefl (mkConst `Bool.true);
h ← mkExpectedTypeHint h decEqTrue;
mkAppM `ofDecideEqTrue #[h]
/-- Return `a < b` -/
def mkLt (a b : Expr) : MetaM Expr :=
mkAppM `HasLess.Less #[a, b]
/-- Return `a <= b` -/
def mkLe (a b : Expr) : MetaM Expr :=
mkAppM `HasLessEq.LessEq #[a, b]
end Meta
end Lean

2
tests/lean/run/meta6.lean
View file

@ -53,7 +53,7 @@ print c;
Meta.check c;
cType ← inferType c;
print cType;
lt ← mkAppM `HasLess.Less #[mkNatLit 10000000, mkNatLit 20000000000];
lt ← mkLt (mkNatLit 10000000) (mkNatLit 20000000000);
ltPrf ← mkDecideProof lt;
Meta.check ltPrf;
t ← inferType ltPrf;