Make tensor opaque

[stschaef]

WIP for making tensor opaque.

We make the definition opaque and propagate that opaqueness throughout the codebase. This changes the type signatures of some things, such as ⊗PathP and Kleene star, as to not leak the details of ⊗. The largest ergonomic changes relate to the inductive types, like Kleene star and NFA parses. The signatures of each constructor must be manually unfolded

  data KL* : Grammar ℓG
    where
    nil : ∀ w → ε w → KL* w
    cons : ∀ w →
      Σ[ s ∈ Splitting w ]
       g (s .fst .fst) × KL* (s .fst .snd) →
      KL* w

The remaining work here seems to be in the Kleene star regex-NFA equivalence

[stschaef]

But the inductive types thing is likely a moot point with the things you just wrote

[maxsnew]

The signatures of each constructor must be manually unfolded

Can you define this instead in an opaque block unfolding tensor?

[stschaef]

The signatures of each constructor must be manually unfolded

Can you define this instead in an opaque block unfolding tensor?

No, because opaque doesn't apply to data declarations

[maxsnew]

Well maybe you can make a non-opaque version of tensor to use in these spots? When you unfold the opaque tensor they will become definitionally equal anyway...Almost anything is better than manually inlining the definition