Gedichte
Musik
Bilder
Quellcodebibliothek
Diashow
Normaldarstellung
products
/
sources
/
formale sprachen
/
Java
/
openjdk-20-36_src
/
src
/
java.desktop
/
share
/
legal
/
Quellcode-Bibliothek
©
Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: bug_3004.v Sprache: Unknown
Set
Implicit
Arguments
.
Unset
Strict
Implicit
.
Parameter
(M : nat ->
Type
).
Parameter
(mp :
forall
(T1 T2 :
Type
) (f : T1 -> T2), list T1 -> list T2).
Definition
foo (s : list {n : nat & M n}) :=
let
exT := existT in mp (
fun
x => projT1 x) s.
[ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet)
]