(* Check that expansion of alias in pattern-matching compilation is no longer dependent of whether the pattern-matching problem occurs in a
typed context or at toplevel (solved from revision 10883) *)
Definition f := fun n m : nat => match n, m with
| O, _ => O
| n, O => n
| _, _ => O end.
Goal f = fun n m : nat => match n, m with
| O, _ => O
| n, O => n
| _, _ => O end. unfold f. reflexivity. Qed.
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.
