aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/SearchPattern.v
blob: 802d8c9760668a32b3e1e63c921ad708049ab8be (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
(* Some tests of the SearchPattern command *)

(* Simple, random tests *)
SearchPattern bool.
SearchPattern nat.
SearchPattern le.

(* With some hypothesis *)
SearchPattern (nat -> nat).
SearchPattern (?n * ?m + ?n = ?n * S ?m).

(* Non-linearity *)
SearchPattern (_ ?X ?X).

(* Non-linearity with hypothesis *)
SearchPattern (forall (x:?A) (y:?B), _ ?A ?B).

(* No delta-reduction *)
SearchPattern (Exc _).