11 lines
127 B
OCaml
11 lines
127 B
OCaml
open Lam
|
|
open Types
|
|
open Proof
|
|
|
|
type cmd =
|
|
| Goal of ty
|
|
| Tact of tactic
|
|
|
|
type parser_entry =
|
|
| Lam of lam
|
|
| Cmd of cmd |