sig
  module Make :
    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
end