Import conflict between Strata and Batteries over List.Forall₂ declarations

[chrissuu]

Hello, I am currently working on writing a frontend targeting Strata, but running into some namespace collision issues.

Summary

Strata and Batteries both define the same inductive in the global List namespace:

List.Forall₂

This makes downstream modules fail if they import Strata/StrataBoole together with a package that imports Batteries.

Repro

import StrataBoole
import Batteries

In our downstream project, this happens through Parser, whose prelude imports all of Batteries:

import StrataBoole
import Parser

The import order changes which side reports the error:

import Batteries.Data.List.Basic failed, environment already contains
'List.Forall₂.below.casesOn' from Strata.DL.Util.List

or:

import Strata.DL.Util.List failed, environment already contains
'List.Forall₂.below.casesOn' from Batteries.Data.List.Basic

Cause

Strata defines:

-- Strata/DL/Util/List.lean
inductive List.Forall₂ (R : α → β → Prop) : List α → List β → Prop where
  | nil : Forall₂ R [] []
  | cons : R a b → Forall₂ R as bs → Forall₂ R (a :: as) (b :: bs)

Batteries also defines List.Forall₂ in Batteries/Data/List/Basic.lean. Lean then collides on generated declarations such as List.Forall₂.below.casesOn.

Impact

We are building a frontend targeting StrataBoole backend and want an in-process Lean embedding. That elaborator needs both our C0 parser stack and StrataDDM/StrataBoole, but the import conflict prevents putting both in one module.

Request

I was wondering if Strata might be open to avoiding the duplicate global List.Forall₂ definition, for example by reusing Batteries' definition when available or moving Strata's version under a Strata-specific namespace?