Set Primitive Projections.
Record params := { width : nat }. Definition p : params := Build_params 64.
Lemma foo : width p = 0 -> width p = 0. intros. let e := lazymatch type of H with ?e = 0 => e end in change tt with tt in H; let E := lazymatch type of H with ?E = 0 => E end in idtac"before:" e; idtac"after :" E; (* before: (width p) *) (* after : (width p) *)
tryif constr_eq e E thenexact H elseidtac. 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.
