products/sources/formale sprachen/PVS/complex_integration/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: recdef.mli   Sprache: Coq

open Constr

val tclUSER_if_not_mes : 
  Tacmach.tactic ->
  bool -> 
  Names.Id.t list option -> 
  Tacmach.tactic
val recursive_definition :  
bool ->
           Names.Id.t ->
           Constrintern.internalization_env ->
           Constrexpr.constr_expr ->
           Constrexpr.constr_expr ->
           int -> Constrexpr.constr_expr -> (pconstant ->
            Indfun_common.tcc_lemma_value ref ->
            pconstant ->
            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option

[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]