products
/
Sources
/
formale Sprachen
/
C
/
LibreOffice
/
cui
/
source
/
options
/ (
LibreOffice
Version 25.8.3.2
©
) Datei vom 5.10.2025 mit Größe 7 kB
Bilddatei
tc.v
products/Sources/formale Sprachen/Roqc/test-suite/ssr/tc.v
(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (*
id x = 0. Proof. Fail move=> _; reflexivity. Timeout 2 rewrite E => _; reflexivity. Qed. Definition P {A} (x : A) : Prop := x = x. Axiom V : forall A {f : foo A} (x:A), P x -> P (id x). Lemma test1 (x : nat) : P x -> P (id x). Proof. move=> px. Timeout 2 Fail move/V: px. Timeout 2 move/V : (px) => _. move/(V nat) : px => H; exact H. Qed.
2026-07-11