Quelle bug_17594.v Sprache: Coq

From Ltac2 Require Import Ltac2.
From Ltac2 Require Import Message.

Ltac2 msg s := print (of_string s).

Goal True.
  (* should be the exact error *)
  Fail multi_match! 'True with
    | True => msg "1"
    | _ => msg "2"
    end;
    msg "3"; exact 0.

  Fail ltac1:(multimatch True with
    | True => idtac "1"
    | _ => idtac "2"
    end; idtac "3"; exact 0).

  Fail multi_match! goal with
    | [ |- True ] => msg "1"
    | [ |- _ ] => msg "2"
    end;
    msg "3"; exact 0.

  Fail ltac1:(multimatch goal with
    | |- True => idtac "1"
    | |- _ => idtac "2"
    end; idtac "3"; exact 0).

  (* should be match error *)
  Fail multi_match! 'True with
    | True => msg "1"
    | False => msg "2"
    end;
    msg "3"; exact 0.

  Fail ltac1:(multimatch True with
    | True => idtac "1"
    | False => idtac "2"
    end; idtac "3"; exact 0).

  Fail multi_match! goal with
    | [ |- True ] => msg "1"
    | [ |- False ] => msg "2"
    end;
    msg "3"; exact 0.

  Fail ltac1:(multimatch goal with
    | |- True => idtac "1"
    | |- False => idtac "2"
    end; idtac "3"; exact 0).

Abort.

quality100%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.