(* To test PP of fixpoints *) RequireImport TestSuite.arith. Checkfix a(n: nat): n<5 -> nat := match n return n<5 -> nat with
| 0 => fun _ => 0
| S n => fun h => S (a n (proj2 (Nat.succ_lt_mono _ _) (Nat.lt_lt_succ_r _ _ h))) end.
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.
