module Context

import Signature
import Term
import Formula

import Data.Fin

%default total

public export
data Context : Signature nFuncs nRels -> Nat -> Type where
  Nil  : Context sig 0
  (::) : {d : Nat} -> Formula sig d -> Context sig n -> Context sig (S n)
  
public export
index : Fin n -> Context sig n -> (d ** Formula sig d)
index FZ (x :: _) = (depth x ** x)
index (FS k) (_ :: xs) = index k xs

public export
data Subset : Context sig n -> Context sig m -> Type where
  Empty   : Subset [] c
  Missing : Subset c1 c2 -> Subset c1 (a :: c2)
  There   : Subset c1 c2 -> Subset (a :: c1) (a :: c2)
  Same    : Subset c c