stdlib/test-suite/output/Search_3.v at master · rocq-prover/stdlib · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

From Stdlib Require Import Morphisms.

Search is:Instance [ Reflexive | Symmetric ].

Module Bug12525.
  (* This was revealing a kernel bug with delta-resolution *)
  Module A. Axiom a:Prop. Axiom b:a. End A.
  Module B. Include A. End B.
  Module M.
    Search B.a.
  End M.
End Bug12525.

From Stdlib Require Lia.

Module Bug12647.
  (* Similar to #12525 *)
  Module Type Foo.
  Axiom P : nat -> Prop.
  Axiom L : P 0.
  End Foo.

  Module Bar (F : Foo).
  Search F.P.
  End Bar.
End Bug12647.

Module WithCoercions.
  Search headconcl:(_ + _) inside Datatypes.
  Coercion Some_nat := @Some nat.
  Axiom f : None = 0.
  Search (None = 0).
End WithCoercions.

From Stdlib Require Import List.

Module Wish13349.
Search partition "1" inside List.
End Wish13349.