package electrod

  1. Overview
  2. Docs
Formal analysis for the Electrod formal pivot language

Install

Dune Dependency

github.com Readme Changelog MPL-2.0 License Edit opam file Versions (10)

Authors

  1. D
    David Chemouil
  2. J
    Julien Brunel

Maintainers

  1. D
    David Chemouil <david.chemouil+git@onera.fr>

Sources

electrod-1.0.0.tbz
sha256=4da251e58d97c797d6e940e586d225a09715777fbb1b25c5527a6a2e1e3c2d58
sha512=89c45ebd0d3401b17eac4217289ed21ec87135ab5fa62bf63b2bed1ad1435a381e3434582c2ec99c2e6d8d87ce23cecfa7ba14d76234493992ae06879b808dd2

doc/electrod.libelectrod/Libelectrod/Elo/class-map/index.html

Class Elo.mapSource

constraint 'c = < visit_'exp : 'env -> exp -> exp ; visit_'fml : 'env -> fml -> fml ; visit_'iexp : 'env -> iexp -> iexp ; visit_Add : 'env -> ibinop ; visit_All : 'env -> quant ; visit_And : 'env -> lbinop ; visit_Block : 'env -> fml list -> (fml, exp, iexp) ofml ; visit_Card : 'env -> exp -> (fml, exp, iexp) oiexp ; visit_Compr : 'env -> (bool * int * exp) list -> fml list -> (fml, exp, iexp) prim_oexp ; visit_Diff : 'env -> rbinop ; visit_F : 'env -> lunop ; visit_FIte : 'env -> fml -> fml -> fml -> (fml, exp, iexp) ofml ; visit_False : 'env -> (fml, exp, iexp) ofml ; visit_G : 'env -> lunop ; visit_Gt : 'env -> icomp_op ; visit_Gte : 'env -> icomp_op ; visit_H : 'env -> lunop ; visit_IBin : 'env -> iexp -> ibinop -> iexp -> (fml, exp, iexp) oiexp ; visit_IComp : 'env -> iexp -> icomp_op -> iexp -> (fml, exp, iexp) ofml ; visit_IEq : 'env -> icomp_op ; visit_INEq : 'env -> icomp_op ; visit_IUn : 'env -> iunop -> iexp -> (fml, exp, iexp) oiexp ; visit_Iden : 'env -> (fml, exp, iexp) prim_oexp ; visit_Iff : 'env -> lbinop ; visit_Imp : 'env -> lbinop ; visit_In : 'env -> comp_op ; visit_Inter : 'env -> rbinop ; visit_Join : 'env -> rbinop ; visit_LBin : 'env -> fml -> lbinop -> fml -> (fml, exp, iexp) ofml ; visit_LProj : 'env -> rbinop ; visit_LUn : 'env -> lunop -> fml -> (fml, exp, iexp) ofml ; visit_Lt : 'env -> icomp_op ; visit_Lte : 'env -> icomp_op ; visit_Name : 'env -> Libelectrod.Name.t -> (fml, exp, iexp) prim_oexp ; visit_Neg : 'env -> iunop ; visit_No : 'env -> quant ; visit_None_ : 'env -> (fml, exp, iexp) prim_oexp ; visit_Not : 'env -> lunop ; visit_NotIn : 'env -> comp_op ; visit_Num : 'env -> int -> (fml, exp, iexp) oiexp ; visit_O : 'env -> lunop ; visit_Or : 'env -> lbinop ; visit_Over : 'env -> rbinop ; visit_P : 'env -> lunop ; visit_Prime : 'env -> exp -> (fml, exp, iexp) prim_oexp ; visit_Prod : 'env -> rbinop ; visit_Quant : 'env -> quant -> (bool * int * exp) -> fml list -> (fml, exp, iexp) ofml ; visit_R : 'env -> lbinop ; visit_RBin : 'env -> exp -> rbinop -> exp -> (fml, exp, iexp) prim_oexp ; visit_RComp : 'env -> exp -> comp_op -> exp -> (fml, exp, iexp) ofml ; visit_REq : 'env -> comp_op ; visit_RIte : 'env -> fml -> exp -> exp -> (fml, exp, iexp) prim_oexp ; visit_RNEq : 'env -> comp_op ; visit_RProj : 'env -> rbinop ; visit_RTClos : 'env -> runop ; visit_RUn : 'env -> runop -> exp -> (fml, exp, iexp) prim_oexp ; visit_S : 'env -> lbinop ; visit_Some_ : 'env -> quant ; visit_Sub : 'env -> ibinop ; visit_T : 'env -> lbinop ; visit_TClos : 'env -> runop ; visit_Transpose : 'env -> runop ; visit_True : 'env -> (fml, exp, iexp) ofml ; visit_U : 'env -> lbinop ; visit_Union : 'env -> rbinop ; visit_Univ : 'env -> (fml, exp, iexp) prim_oexp ; visit_Var : 'env -> int -> (fml, exp, iexp) prim_oexp ; visit_X : 'env -> lunop ; visit_comp_op : 'env -> comp_op -> comp_op ; visit_exp : 'env -> exp -> exp ; visit_fml : 'env -> fml -> fml ; visit_ibinop : 'env -> ibinop -> ibinop ; visit_icomp_op : 'env -> icomp_op -> icomp_op ; visit_iexp : 'env -> iexp -> iexp ; visit_iunop : 'env -> iunop -> iunop ; visit_lbinop : 'env -> lbinop -> lbinop ; visit_lunop : 'env -> lunop -> lunop ; visit_oexp : 'env -> (fml, exp, iexp) oexp -> (fml, exp, iexp) oexp ; visit_ofml : 'env -> (fml, exp, iexp) ofml -> (fml, exp, iexp) ofml ; visit_oiexp : 'env -> (fml, exp, iexp) oiexp -> (fml, exp, iexp) oiexp ; visit_prim_oexp : 'env -> (fml, exp, iexp) prim_oexp -> (fml, exp, iexp) prim_oexp ; visit_quant : 'env -> quant -> quant ; visit_rbinop : 'env -> rbinop -> rbinop ; visit_runop : 'env -> runop -> runop.. >
method visit_'exp : 'env -> exp -> exp
method visit_'fml : 'env -> fml -> fml
method visit_'iexp : 'env -> iexp -> iexp
method visit_Add : 'env -> ibinop
method visit_All : 'env -> quant
method visit_And : 'env -> lbinop
method visit_Block : 'env -> fml list -> (fml, exp, iexp) ofml
method visit_Card : 'env -> exp -> (fml, exp, iexp) oiexp
method visit_Compr : 'env -> (bool * int * exp) list -> fml list -> (fml, exp, iexp) prim_oexp
method visit_Diff : 'env -> rbinop
method visit_F : 'env -> lunop
method visit_FIte : 'env -> fml -> fml -> fml -> (fml, exp, iexp) ofml
method visit_False : 'env -> (fml, exp, iexp) ofml
method visit_G : 'env -> lunop
method visit_Gt : 'env -> icomp_op
method visit_Gte : 'env -> icomp_op
method visit_H : 'env -> lunop
method visit_IBin : 'env -> iexp -> ibinop -> iexp -> (fml, exp, iexp) oiexp
method visit_IComp : 'env -> iexp -> icomp_op -> iexp -> (fml, exp, iexp) ofml
method visit_IEq : 'env -> icomp_op
method visit_INEq : 'env -> icomp_op
method visit_IUn : 'env -> iunop -> iexp -> (fml, exp, iexp) oiexp
method visit_Iden : 'env -> (fml, exp, iexp) prim_oexp
method visit_Iff : 'env -> lbinop
method visit_Imp : 'env -> lbinop
method visit_In : 'env -> comp_op
method visit_Inter : 'env -> rbinop
method visit_Join : 'env -> rbinop
method visit_LBin : 'env -> fml -> lbinop -> fml -> (fml, exp, iexp) ofml
method visit_LProj : 'env -> rbinop
method visit_LUn : 'env -> lunop -> fml -> (fml, exp, iexp) ofml
method visit_Lt : 'env -> icomp_op
method visit_Lte : 'env -> icomp_op
method visit_Name : 'env -> Libelectrod.Name.t -> (fml, exp, iexp) prim_oexp
method visit_Neg : 'env -> iunop
method visit_No : 'env -> quant
method visit_None_ : 'env -> (fml, exp, iexp) prim_oexp
method visit_Not : 'env -> lunop
method visit_NotIn : 'env -> comp_op
method visit_Num : 'env -> int -> (fml, exp, iexp) oiexp
method visit_O : 'env -> lunop
method visit_Or : 'env -> lbinop
method visit_Over : 'env -> rbinop
method visit_P : 'env -> lunop
method visit_Prime : 'env -> exp -> (fml, exp, iexp) prim_oexp
method visit_Prod : 'env -> rbinop
method visit_Quant : 'env -> quant -> (bool * int * exp) -> fml list -> (fml, exp, iexp) ofml
method visit_R : 'env -> lbinop
method visit_RBin : 'env -> exp -> rbinop -> exp -> (fml, exp, iexp) prim_oexp
method visit_RComp : 'env -> exp -> comp_op -> exp -> (fml, exp, iexp) ofml
method visit_REq : 'env -> comp_op
method visit_RIte : 'env -> fml -> exp -> exp -> (fml, exp, iexp) prim_oexp
method visit_RNEq : 'env -> comp_op
method visit_RProj : 'env -> rbinop
method visit_RTClos : 'env -> runop
method visit_RUn : 'env -> runop -> exp -> (fml, exp, iexp) prim_oexp
method visit_S : 'env -> lbinop
method visit_Some_ : 'env -> quant
method visit_Sub : 'env -> ibinop
method visit_T : 'env -> lbinop
method visit_TClos : 'env -> runop
method visit_Transpose : 'env -> runop
method visit_True : 'env -> (fml, exp, iexp) ofml
method visit_U : 'env -> lbinop
method visit_Union : 'env -> rbinop
method visit_Univ : 'env -> (fml, exp, iexp) prim_oexp
method visit_Var : 'env -> int -> (fml, exp, iexp) prim_oexp
method visit_X : 'env -> lunop
method private visit_array : 'env 'a 'b. ('env -> 'a -> 'b) -> 'env -> 'a array -> 'b array
method private visit_bool : 'env. 'env -> bool -> bool
method private visit_bytes : 'env. 'env -> bytes -> bytes
method private visit_char : 'env. 'env -> char -> char
method visit_comp_op : 'env -> comp_op -> comp_op
method visit_exp : 'env -> exp -> exp
method private visit_float : 'env. 'env -> float -> float
method visit_fml : 'env -> fml -> fml
method visit_ibinop : 'env -> ibinop -> ibinop
method visit_icomp_op : 'env -> icomp_op -> icomp_op
method visit_iexp : 'env -> iexp -> iexp
method private visit_int : 'env. 'env -> int -> int
method private visit_int32 : 'env. 'env -> int32 -> int32
method private visit_int64 : 'env. 'env -> int64 -> int64
method visit_iunop : 'env -> iunop -> iunop
method private visit_lazy_t : 'env 'a 'b. ('env -> 'a -> 'b) -> 'env -> 'a lazy_t -> 'b lazy_t
method visit_lbinop : 'env -> lbinop -> lbinop
method private visit_list : 'env 'a 'b. ('env -> 'a -> 'b) -> 'env -> 'a list -> 'b list
method visit_lunop : 'env -> lunop -> lunop
method private visit_nativeint : 'env. 'env -> nativeint -> nativeint
method visit_oexp : 'env -> (fml, exp, iexp) oexp -> (fml, exp, iexp) oexp
method visit_ofml : 'env -> (fml, exp, iexp) ofml -> (fml, exp, iexp) ofml
method visit_oiexp : 'env -> (fml, exp, iexp) oiexp -> (fml, exp, iexp) oiexp
method private visit_option : 'env 'a 'b. ('env -> 'a -> 'b) -> 'env -> 'a option -> 'b option
method visit_prim_oexp : 'env -> (fml, exp, iexp) prim_oexp -> (fml, exp, iexp) prim_oexp
method visit_quant : 'env -> quant -> quant
method visit_rbinop : 'env -> rbinop -> rbinop
method private visit_ref : 'env 'a 'b. ('env -> 'a -> 'b) -> 'env -> 'a ref -> 'b ref
method private visit_result : 'env 'a 'b 'e 'f. ('env -> 'a -> 'b) -> ('env -> 'e -> 'f) -> 'env -> ('a, 'e) result -> ('b, 'f) result
method visit_runop : 'env -> runop -> runop
method private visit_string : 'env. 'env -> string -> string
method private visit_unit : 'env. 'env -> unit -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct