Axioms A B : Type -> Type. Axiom f : A nat -> B Type.
Definition A' := A nat. Definition f' : A' -> B Type := f.
Coercion f' : A' >-> B. Check (_ : A nat) : A'.
Fail Check (_ : A nat) : B Type. (* The term "?11:A nat" has type "A nat" while it is expected to have type "B Type". *) Check ((_ : A nat) : A') : B Type. (* ((?11:A nat):A'):B Type *)
Fail Identity Coercion f'_id : A >-> A'. (* Error: in build_id_coercion: A must be a transparent constant. *)
Identity Coercion f'_id : A' >-> A.
Fail Check (_ : A nat) : B Type. (* The term "?11:A nat" has type "A nat" while it is expected to have type "B Type". *)
Coercion f : A >-> B. (* Warning: f does not respect the uniform inheritance condition *)
Check (_ : A nat) : B Type. (* Anomaly: apply_coercion_args. Please report. *)
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.
