Previous  Up  Next

Module ITM_parser

module ITM_parser: sig .. end

Parser for mapping files containing definitions and proofs to objects of type ITM_types.t_itm list. Generated from ITM_parser.mly with ocamlyacc.

type token =
| EOF
| FML of string
| PRF of string
| DEF of string
| COMMENT of string 
val main : (Stdlib.Lexing.lexbuf -> token) ->
       Stdlib.Lexing.lexbuf -> ITM_types.t_itm list