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