Ltac2 Type foo := [
| #[deprecated(since="bar")] Bar
| #[deprecated(since="baz")] Baz
].
(* can still use foo even if its constructors are deprecated *)
Ltac2 diagonal (x:foo) := (x, x).
(* deprecated constructors warn when using them to construct values *)
Fail Ltac2 nobuild := Bar.
(* deprecated constructors also warn when matching on them *)
Fail Ltac2 nomatch x := match x with
| Bar => 0
| _ => 1 end.
(* warnings are per constructor so we can disable one and not the other
(because this test uses difference "since" annotations) *) Set Warnings "-deprecated-since-bar".
Fail Ltac2 nobuild := Baz.
Ltac2 build_warn_bar_disabled := Bar.
(* warnings are per constructor, so we still can't match on Baz *)
Fail Ltac2 nomatch x := match x with
| Baz => 0
| _ => 1 end.
(* but we can match on Bar with its warning disabled *)
Ltac2 match_warn_bar_disabled x := match x with
| Bar => 0
| _ => 1 end.
(* the warning is at intern time *)
Ltac2 Notation bar_nota := Bar.
Ltac2 Notation"isBar_nota" x(tactic) := match x with Bar => true | _ => false end.
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.
