Definition fact_F : forall (n:nat),
(forall m, m<n -> nat) ->
nat.
refine
(fun n fact_rec => if eq_nat_dec n 0 then
1 else let fn := fact_rec (n-1) _ in
n * fn). Admitted.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
