Skip to content

Commit

Permalink
Add test SearchFixpoint
Browse files Browse the repository at this point in the history
  • Loading branch information
Villetaneuse committed Apr 27, 2024
1 parent f242982 commit ab6d31f
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 0 deletions.
3 changes: 3 additions & 0 deletions test-suite/output/SearchFixpoint.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Foo.bar: nat -> nat
Foo.from: nat -> Foo.Stream
Foo.foo: nat
21 changes: 21 additions & 0 deletions test-suite/output/SearchFixpoint.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
(** Test file for #18983 *)

(** We test that [Search] allows the [is:Fixpoint] and [is:CoFixpoint] search
items while not changing [is:Definition]. *)
Module Foo.
Definition foo := 42.

Fixpoint bar (n : nat) :=
match n with
| 0 => 0
| S n => bar n
end.

(* Example shamelessly taken from the reference manual. *)
CoInductive Stream := Seq : nat -> Stream -> Stream.
CoFixpoint from (n : nat) := Seq n (from (S n)).
End Foo.

Search is:Fixpoint inside Foo.
Search is:CoFixpoint inside Foo.
Search is:Definition inside Foo.

0 comments on commit ab6d31f

Please sign in to comment.