Linearity.agda

dot : ∀ {γ} (Γ Γ′ : Context γ) → Mult
dot ∅ ∅ = 0#
dot (Γ , π ∙ _) (Γ′ , π′ ∙ _) = dot Γ Γ′ + (π * π′)

-- Induction on the size of the output
-- (filling in each item of the output vector)
_⊛′_ : ∀ {γ δ}
  → (Δ : ∀ {B} → δ ∋ B → Context γ)
  → (Γ : Context γ)
  → Context δ
_⊛′_ {γ} {∅} Δ Γ = ∅
_⊛′_ {γ} {δ , _} Δ Γ = ((Δ ∘ S_) ⊛′ Γ) , dot (Δ Z) Γ ∙ _