package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
type loc = Loc.position
type qualid = loc * string list
type pty =
  1. | PTyvar of string
  2. | PTyapp of qualid * pty list
  3. | PTuple of pty list
type metarg =
  1. | PMAty of pty
  2. | PMAfs of qualid
  3. | PMAps of qualid
  4. | PMApr of qualid
  5. | PMAstr of string
  6. | PMAint of int
type th_rule =
  1. | Rprelude of string
  2. | Rsyntaxts of qualid * string * bool
  3. | Rsyntaxfs of qualid * string * bool
  4. | Rsyntaxps of qualid * string * bool
  5. | Rconverter of qualid * string * bool
  6. | Rliteral of qualid * string * bool
  7. | Rremovepr of qualid
  8. | Rremoveall
  9. | Rmeta of string * metarg list
  10. | Ruse of qualid
type theory_rules = {
  1. thr_name : qualid;
  2. thr_rules : (loc * th_rule) list;
}
type mo_rule =
  1. | MRtheory of th_rule
  2. | MRinterface of string
  3. | MRexception of qualid * string
  4. | MRval of qualid * string
type module_rules = {
  1. mor_name : qualid;
  2. mor_rules : (loc * mo_rule) list;
}
type global =
  1. | Prelude of string
  2. | Printer of string
  3. | ModelParser of string
  4. | RegexpValid of string
  5. | RegexpInvalid of string
  6. | RegexpTimeout of string
  7. | RegexpOutOfMemory of string
  8. | RegexpStepLimitExceeded of string
  9. | RegexpUnknown of string * string
  10. | RegexpFailure of string * string
  11. | TimeRegexp of string
  12. | StepRegexp of string * int
  13. | ExitCodeValid of int
  14. | ExitCodeInvalid of int
  15. | ExitCodeTimeout of int
  16. | ExitCodeStepLimitExceeded of int
  17. | ExitCodeUnknown of int * string
  18. | ExitCodeFailure of int * string
  19. | Filename of string
  20. | Transform of string
  21. | Plugin of string * string
  22. | Blacklist of string list
type file = {
  1. f_global : (loc * global) list;
  2. f_rules : theory_rules list;
}
type global_extract =
  1. | EPrelude of string
  2. | EPrinter of string
  3. | EBlacklist of string list
type file_extract = {
  1. fe_global : (loc * global_extract) list;
  2. fe_th_rules : theory_rules list;
  3. fe_mo_rules : module_rules list;
}
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