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 650 B image not shown  

Quelle  bug7348.out   Sprache: unbekannt

 
Spracherkennung für: .out vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]

Extracted code successfully compiled

type __ = Obj.t

type unit0 =
| Tt

type bool =
| True
| False

module Case1 =
 struct
  type coq_rec = { f : bool }

  (** val f : bool -> coq_rec -> bool **)

  let f _ r =
    r.f

  (** val silly : bool -> coq_rec -> __ **)

  let silly x b =
    match x with
    | True -> Obj.magic b.f
    | False -> Obj.magic Tt
 end

module Case2 =
 struct
  type coq_rec = { f : (bool -> bool) }

  (** val f : bool -> coq_rec -> bool -> bool **)

  let f _ r =
    r.f

  (** val silly : bool -> coq_rec -> __ **)

  let silly x b =
    match x with
    | True -> Obj.magic b.f False
    | False -> Obj.magic Tt
 end


[ Dauer der Verarbeitung: 0.52 Sekunden  ]