package why3

  1. Overview
  2. Docs
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_literal
  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.integer_literal
  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 ident_comma_list_eof : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Ptree.ident list
module MenhirInterpreter : sig ... end
module Incremental : sig ... end
OCaml

Innovation. Community. Security.