Quellcodebibliothek
Statistik
Leitseite
products
/
Sources
/
formale Sprachen
/
C
/
Linux
/
drivers
/
pinctrl
/
mediatek
/ (
Open Source Betriebssystem
Version 6.17.9
©
) Datei vom 24.10.2025 mit Größe 13 kB
Bilddatei
ipat_apply.v
products/Sources/formale Sprachen/Roqc/test-suite/ssr/ipat_apply.v
Require Import ssreflect. Section Apply. Variable P : nat -> Prop. Lemma test_apply A B : forall (f : A -> B) (a : A), B. Proof. move=> /[apply] b. exact. Qed. End Apply.
2026-05-26