Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: converse_zorn.prf   Sprache: SML

Untersuchung Coq©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Ccalgo
open Constr

type rule=
    Ax of constr
  | SymAx of constr
  | Refl of term
  | Trans of proof*proof
  | Congr of proof*proof
  | Inject of proof*pconstructor*int*int
and proof =
    private {p_lhs:term;p_rhs:term;p_rule:rule}

(** Proof smart constructors *)

val prefl:term -> proof

val pcongr: proof -> proof -> proof

val ptrans: proof -> proof -> proof

val psym: proof -> proof

val pax : (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t ->
           Ccalgo.Constrhash.key -> proof

val psymax :  (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t ->
           Ccalgo.Constrhash.key -> proof

val pinject :  proof -> pconstructor -> int -> int -> proof

(** Proof building functions *)

val equal_proof : Environ.env -> Evd.evar_map -> forest -> int -> int -> proof

val edge_proof : Environ.env -> Evd.evar_map -> forest -> (int*int)*equality -> proof

val path_proof : Environ.env -> Evd.evar_map -> forest -> int -> ((int*int)*equality) list -> proof

val congr_proof : Environ.env -> Evd.evar_map -> forest -> int -> int -> proof

val ind_proof : Environ.env -> Evd.evar_map -> forest -> int -> pa_constructor -> int -> pa_constructor -> proof

(** Main proof building function *)

val build_proof :
  Environ.env -> Evd.evar_map -> forest ->
  [ `Discr of int * pa_constructor * int * pa_constructor
  | `Prove of int * int ] -> proof


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤





Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik