Section A.
Context {a : nat}. Section B.
Context {b : nat}. Definition foo (eq1 : a = a) (eq2 : b = b) (c : nat) : c = c := eq_refl. GlobalArguments foo _ {_} {d} : rename. End B. End A. Arguments foo. (* was raising an anomaly *) Check foo _ (d:=0). (* was wrongly binding d to eq2 *)
Fail Check foo (eq1 := 3) (eq_refl 2) (eq_refl 3) 4. (* was wrongly binding eq1 to b *)
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.
