14 lines
208 B
OCaml
14 lines
208 B
OCaml
open Structs;;
|
|
|
|
type tactic =
|
|
| Intro of var_lambda
|
|
| Intros of var_lambda list
|
|
| Assumption
|
|
| Apply of var_lambda
|
|
| Elim of var_lambda
|
|
| Cut of ty
|
|
| Split
|
|
| Left
|
|
| Right
|
|
| Exact of lam;;
|