test(tests/lean/bad_eqns): add tests for definition package error messages

tests/lean/bad_eqns.lean

@@ -0,0 +1,36 @@
+open nat
+
+definition foo : nat → nat,
+foo (0 + x) := x
+
+definition foo : nat → nat → nat,
+foo 0 _   := 0,
+foo x ⌞y⌟ := x
+
+definition foo : nat → nat → nat,
+foo 0   _ := 0,
+foo ⌞x⌟ x := x
+
+inductive tree (A : Type) :=
+node   : tree_list A → tree A,
+leaf   : A → tree A
+with tree_list :=
+nil {} : tree_list A,
+cons   : tree A → tree_list A → tree_list A
+
+definition is_leaf {A : Type} : tree A → bool
+with is_leaf_aux : tree_list A → bool,
+is_leaf (tree.node _)            := bool.ff,
+is_leaf (tree.leaf _)            := bool.tt,
+is_leaf_aux tree_list.nil        := bool.ff,
+is_leaf_aux (tree_list.cons _ _) := bool.ff
+
+definition foo : nat → nat,
+foo 0     := 0,
+foo (x+1) := let y := x + 2 in y * y
+
+example : foo 5 = 36 := rfl
+
+definition boo : nat → nat,
+boo (x + 1) := boo (x + 2),
+boo 0       := 0

tests/lean/bad_eqns.lean.expected.out

@@ -0,0 +1,9 @@
+bad_eqns.lean:4:0: error: invalid argument, it is not a constructor, variable, nor it is marked as an inaccessible pattern
+  0 + x
+in the following equation left-hand-side
+  foo (0 + x)
+bad_eqns.lean:8:0: error: invalid equation left-hand-side, variable 'y' only occurs in inaccessible terms in the following equation left-hand-side
+  foo x y
+bad_eqns.lean:10:11: error: invalid recursive equations for 'foo', inconsistent use of inaccessible term annotation, in some equations a pattern is a constructor, and in another it is an inaccessible term
+bad_eqns.lean:21:11: error: mutual recursion is not needed when defining non-recursive functions
+bad_eqns.lean:34:11: error: invalid recursive equations, failed to find recursive arguments that are structurally smaller (possible solution: use well-founded recursion)