package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
type token =
  1. | WRITES
  2. | WITH
  3. | WHILE
  4. | VARIANT
  5. | VAL
  6. | USE
  7. | UNDERSCORE
  8. | UIDENT of string
  9. | TYPE
  10. | TRY
  11. | TRUE
  12. | TO
  13. | THEORY
  14. | THEN
  15. | STRING of string
  16. | SO
  17. | SEMICOLON
  18. | SCOPE
  19. | RIGHTSQ_QUOTE of string
  20. | RIGHTSQ
  21. | RIGHTPAR_USCORE of string
  22. | RIGHTPAR_QUOTE of string
  23. | RIGHTPAR
  24. | RIGHTBRC
  25. | RETURNS
  26. | RETURN
  27. | REQUIRES
  28. | REF
  29. | REC
  30. | REAL of Number.real_constant
  31. | READS
  32. | RANGE
  33. | RAISES
  34. | RAISE
  35. | QUOTE_LIDENT of string
  36. | PURE
  37. | PRIVATE
  38. | PREDICATE
  39. | POSITION of Loc.position
  40. | PARTIAL
  41. | OR
  42. | OPPREF of string
  43. | OP4 of string
  44. | OP3 of string
  45. | OP2 of string
  46. | OP1 of string
  47. | OLD
  48. | NOT
  49. | MUTABLE
  50. | MODULE
  51. | MINUS
  52. | META
  53. | MATCH
  54. | LTGT
  55. | LT
  56. | LRARROW
  57. | LIDENT of string
  58. | LET
  59. | LEMMA
  60. | LEFTSQ
  61. | LEFTPAR
  62. | LEFTBRC
  63. | LARROW
  64. | LABEL
  65. | INVARIANT
  66. | INTEGER of Number.int_constant
  67. | INDUCTIVE
  68. | IN
  69. | IMPORT
  70. | IF
  71. | GT
  72. | GOAL
  73. | GHOST
  74. | FUNCTION
  75. | FUN
  76. | FORALL
  77. | FOR
  78. | FLOAT
  79. | FALSE
  80. | EXPORT
  81. | EXISTS
  82. | EXCEPTION
  83. | EQUAL
  84. | EPSILON
  85. | EOF
  86. | ENSURES
  87. | END
  88. | ELSE
  89. | DOWNTO
  90. | DOTDOT
  91. | DOT
  92. | DONE
  93. | DO
  94. | DIVERGES
  95. | CORE_UIDENT of string
  96. | CORE_LIDENT of string
  97. | CONTINUE
  98. | CONSTANT
  99. | COMMA
  100. | COLON
  101. | COINDUCTIVE
  102. | CLONE
  103. | CHECK
  104. | BY
  105. | BREAK
  106. | BEGIN
  107. | BARBAR
  108. | BAR
  109. | AXIOM
  110. | ATTRIBUTE of string
  111. | AT
  112. | ASSUME
  113. | ASSERT
  114. | AS
  115. | ARROW
  116. | ANY
  117. | AND
  118. | AMPAMP
  119. | AMP
  120. | ALIAS
  121. | ABSURD
  122. | ABSTRACT
exception Error
val term_eof : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Ptree.term
val term_comma_list_eof : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Ptree.term list
val qualid_eof : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Ptree.qualid
val qualid_comma_list_eof : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Ptree.qualid list
val mlw_file_parsing_only : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Ptree.mlw_file
val ident_comma_list_eof : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Ptree.ident list
val decl_eof : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Ptree.decl
module MenhirInterpreter : sig ... end
module Incremental : sig ... end
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