From 0f56b5f5b7a91f00289a2b680ab0fb4fe01bb36b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Nov 2014 14:27:05 -0800
Subject: [PATCH] test(tests/lean/run): add structure command test

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

diff --git a/tests/lean/run/record1.lean b/tests/lean/run/record1.lean
new file mode 100644
index 000000000..2f70dcf69
--- /dev/null
+++ b/tests/lean/run/record1.lean
@@ -0,0 +1,44 @@
+import logic data.unit
+
+
+structure point (A : Type) (B : Type) :=
+mk :: (x : A) (y : B)
+
+check point
+check point.rec
+check point.mk
+check point.x
+check point.y
+check point.rec_on
+check point.induction_on
+check point.cases_on
+
+inductive color :=
+red, green, blue
+
+structure color_point (A : Type) (B : Type) extends point A B :=
+mk :: (c : color)
+
+check @color_point.rec_on
+check color_point.rec_on
+
+section
+variables a b : num
+
+example : point.x (point.mk a b) = a :=
+rfl
+
+example : point.y (point.mk a b) = b :=
+rfl
+
+variables cc : color
+
+example : color_point.x (color_point.mk a b cc) = a :=
+rfl
+
+example : color_point.y (color_point.mk a b cc) = b :=
+rfl
+
+example : color_point.c (color_point.mk a b cc) = cc :=
+rfl
+end