From 6b18f486d11c13a075aaa4e1462af6c2cbb72cbc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 7 Aug 2020 14:46:11 -0700
Subject: [PATCH] feat: add `mkLt` and `mkLe`

---
 src/Lean/Meta/AppBuilder.lean | 8 ++++++++
 tests/lean/run/meta6.lean     | 2 +-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 617e0712d2..894c0f458b 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -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
diff --git a/tests/lean/run/meta6.lean b/tests/lean/run/meta6.lean
index 50af2e051f..747516b338 100644
--- a/tests/lean/run/meta6.lean
+++ b/tests/lean/run/meta6.lean
@@ -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;