Skip to content

Enable `map_Forall2` to be used in nested inductive relations

Robbert Krebbers requested to merge robbert/map_Forall2_nested into master

This MR allows definitions like the following, whereas they were previously rejected by the positivity checker:

Inductive gtest_rel `{Countable K} : relation (gtest K) :=
  | GTest_rel ts1 ts2 :
     map_Forall2 (λ _, gtest_rel) ts1 ts2 → gtest_rel (GTest ts1) (GTest ts2).

Merge request reports