Definition prod_map {A A' B B'} (f : A -> A') (g : B -> B')
(p : A * B) : A' * B'
:= (f (fst p), g (snd p)). Arguments prod_map {_ _ _ _} _ _ !_ /.
Lemma test1 {A A' B B'} (f : A -> A') (g : B -> B') x y :
prod_map f g (x,y) = (f x, g y). Proof.
Succeed progress simpl; matchgoalwith |- ?x = ?x => idtacend. (* LHS becomes (f x, g y) *)
Succeed progress cbn; matchgoalwith |- ?x = ?x => idtacend. (* LHS is not simplified *) Admitted.
Axiom n : nat. Arguments Nat.add _ !_.
Goal n + S n = 0.
Fail progress cbn. Abort.
Goal S n + S n = 0.
progress cbn. matchgoalwith |- S (n + S n) = 0 => idtacend. Abort.
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.
