Up  

Module Reduce.Make.Full

module Full: sig .. end
val whnf : ?subst:Reduce.Make.subst ->
       T.t ->
       T.t list -> T.t * T.t list * Reduce.Make.subst * T.t TermInner.Builtin.guard
whnf f l applies f to l and returns its WHNF, as a tuple f', l', subst, guard where f l ---> subst ((f guard) l)