From 5e36b905100358d8517cf859c2bde73bde6137d1 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sun, 29 Sep 2024 19:12:26 +0200 Subject: [PATCH] Also add a test for `map_Forall`. --- tests/fin_maps.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/tests/fin_maps.v b/tests/fin_maps.v index f3f96233..80b00c33 100644 --- a/tests/fin_maps.v +++ b/tests/fin_maps.v @@ -440,8 +440,13 @@ Fixpoint gtest_imap `{Countable K} (j : K) (t : gtest K) : gtest K := let '(GTest ts) := t in GTest (map_imap (λ i t, guard (i = j);; Some (gtest_imap j t)) ts). -(** Test that [map_Forall2] can be used in an inductive definition without +(** Test that [map_Forall P] and [map_Forall2 P] can be used in an inductive +definition with a recursive occurence in the predicate/relation [P] without bothering the positivity checker. *) +Inductive gtest_pred `{Countable K} : gtest K → Prop := + | GTest_pred ts : + map_Forall (λ _, gtest_pred) ts → gtest_pred (GTest ts). + Inductive gtest_rel `{Countable K} : relation (gtest K) := | GTest_rel ts1 ts2 : map_Forall2 (λ _, gtest_rel) ts1 ts2 → gtest_rel (GTest ts1) (GTest ts2). -- GitLab