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. | REC
  29. | REAL of Number.real_literal
  30. | READS
  31. | RANGE
  32. | RAISES
  33. | RAISE
  34. | QUOTE_LIDENT of string
  35. | PURE
  36. | PRIVATE
  37. | PREDICATE
  38. | POSITION of Loc.position
  39. | PARTIAL
  40. | OR
  41. | OPPREF of string
  42. | OP4 of string
  43. | OP3 of string
  44. | OP2 of string
  45. | OP1 of string
  46. | OLD
  47. | NOT
  48. | MUTABLE
  49. | MODULE
  50. | MINUS
  51. | META
  52. | MATCH
  53. | LTGT
  54. | LT
  55. | LRARROW
  56. | LIDENT of string
  57. | LET
  58. | LEMMA
  59. | LEFTSQ
  60. | LEFTPAR
  61. | LEFTBRC
  62. | LARROW
  63. | LABEL
  64. | INVARIANT
  65. | INTEGER of Number.integer_literal
  66. | INDUCTIVE
  67. | IN
  68. | IMPORT
  69. | IF
  70. | GT
  71. | GOAL
  72. | GHOST
  73. | FUNCTION
  74. | FUN
  75. | FORALL
  76. | FOR
  77. | FLOAT
  78. | FALSE
  79. | EXPORT
  80. | EXISTS
  81. | EXCEPTION
  82. | EQUAL
  83. | EPSILON
  84. | EOF
  85. | ENSURES
  86. | END
  87. | ELSE
  88. | DOWNTO
  89. | DOTDOT
  90. | DOT
  91. | DONE
  92. | DO
  93. | DIVERGES
  94. | CORE_UIDENT of string
  95. | CORE_LIDENT of string
  96. | CONTINUE
  97. | CONSTANT
  98. | COMMA
  99. | COLON
  100. | COINDUCTIVE
  101. | CLONE
  102. | CHECK
  103. | BY
  104. | BREAK
  105. | BEGIN
  106. | BARBAR
  107. | BAR
  108. | AXIOM
  109. | ATTRIBUTE of string
  110. | AT
  111. | ASSUME
  112. | ASSERT
  113. | AS
  114. | ARROW
  115. | ANY
  116. | AND
  117. | AMPAMP
  118. | ALIAS
  119. | ABSURD
  120. | 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.