functor Rules
  (structure Ctx' : CTX
   structure Seq' : SEQ
     sharing Seq'.Ctx = Ctx')
  : RULES =
struct

  structure Ctx = Ctx'
  structure Seq = Seq'
  
  local
    open Ctx
    infix $
    structure Term = Seq.Prop.Term
    structure Prop = Seq.Prop
  in
    type hyp = int
    type hyps = hyp list
    type split = hyps * hyps

    fun initial _ = raise Seq.Fail ("NYI")
    fun derelict _ _ = raise Seq.Fail ("NYI")
    fun tensorR _ _ = raise Seq.Fail ("NYI")
    fun tensorL _ _ = raise Seq.Fail ("NYI")
    fun lolliR _ = raise Seq.Fail ("NYI")
    fun lolliL _ _ _ = raise Seq.Fail ("NYI")
    fun oneR _ = raise Seq.Fail ("NYI")
    fun oneL _ = raise Seq.Fail ("NYI")
    fun withR _ = raise Seq.Fail ("NYI")
    fun withL1 _ _ = raise Seq.Fail ("NYI")
    fun withL2 _ _ = raise Seq.Fail ("NYI")
    fun topR _ = raise Seq.Fail ("NYI")
    fun plusR1 _ = raise Seq.Fail ("NYI")
    fun plusR2 _ = raise Seq.Fail ("NYI")
    fun plusL _ _ = raise Seq.Fail ("NYI")
    fun zeroL _ = raise Seq.Fail ("NYI")
    fun impliesR _ = raise Seq.Fail ("NYI")
    fun impliesL _ _ = raise Seq.Fail ("NYI")
    fun bangR _ = raise Seq.Fail ("NYI")
    fun bangL _ _ = raise Seq.Fail ("NYI")
    fun forallR _ _ = raise Seq.Fail ("NYI")
    fun forallL _ _ _ = raise Seq.Fail ("NYI")
    fun existsR _ _ = raise Seq.Fail ("NYI")
    fun existsL _ _ _ = raise Seq.Fail ("NYI")

  end  (* local open ... *)
end;  (* functor RULES *)