products/Sources/formale Sprachen/Coq/test-suite/ide/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ssrpattern.v   Sprache: Unknown

Require Import ssrmatching.

Goal forall n, match n with 0 => 0 | _ => 0 end = 0.
Proof.
  intro n.
  ssrpattern (match _ with 0 => _ | S n' => _ end).
Abort.

[ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ]