| 12345678910111213141516171819202122232425262728293031323334 |
- module Pat (BaseType : Set) where
- data Ty : Set where
- ι : BaseType -> Ty
- _⟶_ : Ty -> Ty -> Ty
- data Bwd (A : Set) : Set where
- • : Bwd A
- _◄_ : Bwd A -> A -> Bwd A
- infixl 30 _◄_
- Ctx = Bwd Ty
- data Take {A : Set} : Bwd A -> A -> Bwd A -> Set where
- hd : forall {x xs} -> Take (xs ◄ x) x xs
- tl : forall {x y xs ys} -> Take xs x ys -> Take (xs ◄ y) x (ys ◄ y)
- data Pat : Ctx -> Ctx -> Ty -> Ctx -> Set
- data Pats : Ctx -> Ty -> Ctx -> Ty -> Set where
- ε : forall {Θ τ} -> Pats Θ τ Θ τ
- _,_ : forall {Θ₁ Θ₂ Θ₃ ρ σ τ} ->
- Pat • Θ₁ ρ Θ₂ -> Pats Θ₂ σ Θ₃ τ ->
- Pats Θ₁ (ρ ⟶ σ) Θ₃ τ
- data Pat where
- ƛ : forall {Δ Θ Θ' σ τ} -> Pat (Δ ◄ σ) Θ τ Θ' ->
- Pat Δ Θ (σ ⟶ τ) Θ'
- _[_] : forall {Θ Θ' Δ σ τ} ->
- Take Θ σ Θ' -> Pats Δ σ • τ -> Pat Δ Θ τ Θ'
|
