functor (T : TermInner.S) ->
  sig
    type subst = (T.t, T.t) Var.Subst.t
    val whnf : ?subst:Reduce.Make.subst -> T.t -> T.t
    val snf : ?subst:Reduce.Make.subst -> T.t -> T.t
    val app_whnf : ?subst:Reduce.Make.subst -> T.t -> T.t list -> T.t
    val eta_reduce : T.t -> T.t
    module Full :
      sig
        val whnf :
          ?subst:Reduce.Make.subst ->
          T.t ->
          T.t list ->
          T.t * T.t list * Reduce.Make.subst * T.t TermInner.Builtin.guard
      end
  end