From af391fe812925eff875175249c8c24329e1cf763 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 25 Apr 2021 20:35:13 -0700
Subject: [PATCH] test: reflective inductive predicate

---
 tests/lean/run/reflectiveIndPred.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 tests/lean/run/reflectiveIndPred.lean

diff --git a/tests/lean/run/reflectiveIndPred.lean b/tests/lean/run/reflectiveIndPred.lean
new file mode 100644
index 0000000000..09d484100a
--- /dev/null
+++ b/tests/lean/run/reflectiveIndPred.lean
@@ -0,0 +1,12 @@
+inductive Expr where
+  | val : Nat → Expr
+  | add : Expr → Expr → Expr
+  | fn  : (Nat → Expr) → Expr
+
+inductive Pos : Expr → Prop
+  | base : (n : Nat) → Pos (Expr.val n.succ)
+  | add  : Pos e₁ → Pos e₂ → Pos (Expr.add e₁ e₂)
+  | fn   : ((n : Nat) → Pos (f n)) → Pos (Expr.fn f)
+
+#print PosProofBelow
+#print Pos.brecOn