Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/output/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 683 B image not shown  

SSL Implicit.out   Sprache: unbekannt

 
rahmenlose Ansicht.out DruckansichtUnknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]

compose S
     : (nat -> nat) -> nat -> nat
ex_intro (P:=fun _ : nat => True) (x:=0) I
     : ex (fun _ : nat => True)
d2 = fun x : nat => d1 (y:=x)
     : forall [x x0 : nat], x0 = x -> x0 = x

Arguments d2 [x x]%_nat_scope h
map id (1 :: nil)
     : list nat
map id' (1 :: nil)
     : list nat
map (id'' (A:=nat)) (1 :: nil)
     : list nat
fix f (x : nat) : option nat := match x with
                                | 0 => None
                                | S _ => x
                                end
     : nat -> option nat
fun x : False => let y := False_rect (A:=bool) x in y
     : False -> bool
fun x : False => let y : True := False_rect x in y
     : False -> True

[ Verzeichnis aufwärts0.96unsichere Verbindung  ]