package electrod
Formal analysis for the Electrod formal pivot language
Install
Dune Dependency
Authors
Maintainers
Sources
electrod-1.0.0.tbz
sha256=4da251e58d97c797d6e940e586d225a09715777fbb1b25c5527a6a2e1e3c2d58
sha512=89c45ebd0d3401b17eac4217289ed21ec87135ab5fa62bf63b2bed1ad1435a381e3434582c2ec99c2e6d8d87ce23cecfa7ba14d76234493992ae06879b808dd2
doc/electrod.libelectrod/Libelectrod/Elo/class-fold/index.html
Class Elo.foldSource
constraint
'c =
< build_Add : 'env -> 'g
; build_All : 'env -> 'h
; build_And : 'env -> 'i
; build_Block : 'env -> 'j list -> 'j
; build_Card : 'env -> 'k -> 'l
; build_Compr : 'env -> (bool * int * 'k) list -> 'j list -> 'm
; build_Diff : 'env -> 'n
; build_F : 'env -> 'o
; build_FIte : 'env -> 'j -> 'j -> 'j -> 'j
; build_False : 'env -> 'j
; build_G : 'env -> 'o
; build_Gt : 'env -> 'p
; build_Gte : 'env -> 'p
; build_H : 'env -> 'o
; build_IBin : 'env -> 'l -> 'g -> 'l -> 'l
; build_IComp : 'env -> 'l -> 'p -> 'l -> 'j
; build_IEq : 'env -> 'p
; build_INEq : 'env -> 'p
; build_IUn : 'env -> 'q -> 'l -> 'l
; build_Iden : 'env -> 'm
; build_Iff : 'env -> 'i
; build_Imp : 'env -> 'i
; build_In : 'env -> 'r
; build_Inter : 'env -> 'n
; build_Join : 'env -> 'n
; build_LBin : 'env -> 'j -> 'i -> 'j -> 'j
; build_LProj : 'env -> 'n
; build_LUn : 'env -> 'o -> 'j -> 'j
; build_Lt : 'env -> 'p
; build_Lte : 'env -> 'p
; build_Name : 'env -> Libelectrod.Name.t -> 'm
; build_Neg : 'env -> 'q
; build_No : 'env -> 'h
; build_None_ : 'env -> 'm
; build_Not : 'env -> 'o
; build_NotIn : 'env -> 'r
; build_Num : 'env -> int -> 'l
; build_O : 'env -> 'o
; build_Or : 'env -> 'i
; build_Over : 'env -> 'n
; build_P : 'env -> 'o
; build_Prime : 'env -> 'k -> 'm
; build_Prod : 'env -> 'n
; build_Quant : 'env -> 'h -> (bool * int * 'k) -> 'j list -> 'j
; build_R : 'env -> 'i
; build_RBin : 'env -> 'k -> 'n -> 'k -> 'm
; build_RComp : 'env -> 'k -> 'r -> 'k -> 'j
; build_REq : 'env -> 'r
; build_RIte : 'env -> 'j -> 'k -> 'k -> 'm
; build_RNEq : 'env -> 'r
; build_RProj : 'env -> 'n
; build_RTClos : 'env -> 's
; build_RUn : 'env -> 's -> 'k -> 'm
; build_S : 'env -> 'i
; build_Some_ : 'env -> 'h
; build_Sub : 'env -> 'g
; build_T : 'env -> 'i
; build_TClos : 'env -> 's
; build_Transpose : 'env -> 's
; build_True : 'env -> 'j
; build_U : 'env -> 'i
; build_Union : 'env -> 'n
; build_Univ : 'env -> 'm
; build_Var : 'env -> int -> 'm
; build_X : 'env -> 'o
; build_oexp : 'env -> 'm -> int -> 'k
; visit_'exp : 'env -> exp -> 'k
; visit_'fml : 'env -> fml -> 'j
; visit_'iexp : 'env -> iexp -> 'l
; visit_Add : 'env -> 'g
; visit_All : 'env -> 'h
; visit_And : 'env -> 'i
; visit_Block : 'env -> fml list -> 'j
; visit_Card : 'env -> exp -> 'l
; visit_Compr : 'env -> (bool * int * exp) list -> fml list -> 'm
; visit_Diff : 'env -> 'n
; visit_F : 'env -> 'o
; visit_FIte : 'env -> fml -> fml -> fml -> 'j
; visit_False : 'env -> 'j
; visit_G : 'env -> 'o
; visit_Gt : 'env -> 'p
; visit_Gte : 'env -> 'p
; visit_H : 'env -> 'o
; visit_IBin : 'env -> iexp -> ibinop -> iexp -> 'l
; visit_IComp : 'env -> iexp -> icomp_op -> iexp -> 'j
; visit_IEq : 'env -> 'p
; visit_INEq : 'env -> 'p
; visit_IUn : 'env -> iunop -> iexp -> 'l
; visit_Iden : 'env -> 'm
; visit_Iff : 'env -> 'i
; visit_Imp : 'env -> 'i
; visit_In : 'env -> 'r
; visit_Inter : 'env -> 'n
; visit_Join : 'env -> 'n
; visit_LBin : 'env -> fml -> lbinop -> fml -> 'j
; visit_LProj : 'env -> 'n
; visit_LUn : 'env -> lunop -> fml -> 'j
; visit_Lt : 'env -> 'p
; visit_Lte : 'env -> 'p
; visit_Name : 'env -> Libelectrod.Name.t -> 'm
; visit_Neg : 'env -> 'q
; visit_No : 'env -> 'h
; visit_None_ : 'env -> 'm
; visit_Not : 'env -> 'o
; visit_NotIn : 'env -> 'r
; visit_Num : 'env -> int -> 'l
; visit_O : 'env -> 'o
; visit_Or : 'env -> 'i
; visit_Over : 'env -> 'n
; visit_P : 'env -> 'o
; visit_Prime : 'env -> exp -> 'm
; visit_Prod : 'env -> 'n
; visit_Quant : 'env -> quant -> (bool * int * exp) -> fml list -> 'j
; visit_R : 'env -> 'i
; visit_RBin : 'env -> exp -> rbinop -> exp -> 'm
; visit_RComp : 'env -> exp -> comp_op -> exp -> 'j
; visit_REq : 'env -> 'r
; visit_RIte : 'env -> fml -> exp -> exp -> 'm
; visit_RNEq : 'env -> 'r
; visit_RProj : 'env -> 'n
; visit_RTClos : 'env -> 's
; visit_RUn : 'env -> runop -> exp -> 'm
; visit_S : 'env -> 'i
; visit_Some_ : 'env -> 'h
; visit_Sub : 'env -> 'g
; visit_T : 'env -> 'i
; visit_TClos : 'env -> 's
; visit_Transpose : 'env -> 's
; visit_True : 'env -> 'j
; visit_U : 'env -> 'i
; visit_Union : 'env -> 'n
; visit_Univ : 'env -> 'm
; visit_Var : 'env -> int -> 'm
; visit_X : 'env -> 'o
; visit_comp_op : 'env -> comp_op -> 'r
; visit_exp : 'env -> exp -> 'k
; visit_fml : 'env -> fml -> 'j
; visit_ibinop : 'env -> ibinop -> 'g
; visit_icomp_op : 'env -> icomp_op -> 'p
; visit_iexp : 'env -> iexp -> 'l
; visit_iunop : 'env -> iunop -> 'q
; visit_lbinop : 'env -> lbinop -> 'i
; visit_lunop : 'env -> lunop -> 'o
; visit_oexp : 'env -> (fml, exp, iexp) oexp -> 'k
; visit_ofml : 'env -> (fml, exp, iexp) ofml -> 'j
; visit_oiexp : 'env -> (fml, exp, iexp) oiexp -> 'l
; visit_prim_oexp : 'env -> (fml, exp, iexp) prim_oexp -> 'm
; visit_quant : 'env -> quant -> 'h
; visit_rbinop : 'env -> rbinop -> 'n
; visit_runop : 'env -> runop -> 's.. >method virtual build_Name : 'env -> Libelectrod.Name.t -> 'mmethod visit_'exp : 'env -> exp -> 'kmethod visit_'fml : 'env -> fml -> 'jmethod visit_'iexp : 'env -> iexp -> 'lmethod visit_Block : 'env -> fml list -> 'jmethod visit_Card : 'env -> exp -> 'lmethod visit_Name : 'env -> Libelectrod.Name.t -> 'mmethod visit_Prime : 'env -> exp -> 'mmethod visit_comp_op : 'env -> comp_op -> 'rmethod visit_exp : 'env -> exp -> 'kmethod visit_fml : 'env -> fml -> 'jmethod visit_ibinop : 'env -> ibinop -> 'gmethod visit_icomp_op : 'env -> icomp_op -> 'pmethod visit_iexp : 'env -> iexp -> 'lmethod visit_iunop : 'env -> iunop -> 'qmethod visit_lbinop : 'env -> lbinop -> 'imethod visit_lunop : 'env -> lunop -> 'omethod visit_quant : 'env -> quant -> 'hmethod visit_rbinop : 'env -> rbinop -> 'nmethod visit_runop : 'env -> runop -> 's