| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/theories/Ltac2/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 1 kB |
|
Quelle Ltac1CompatNotations.v Sprache: Coq |
|||||||||||||||
|
(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This file contains Ltac2 Notations reproducing Ltac1 parsing of tactics, that can be harmful to parsing, and produce bad error messages. They should hence only be imported to port proof script written in Ltac1, or if they are really wanted. *) Require Import Ltac2.Init Ltac2.Std. Ltac2 Notation "transitivity" c(constr) : 1 := Std.transitivity c. Ltac2 Notation "rename" renames(list1(seq(ident, "into", ident), ",")) := Std.rename renames.
¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-04-04