pieuvre/parser_entry.ml

open Lam
open Types
open Proof

type cmd =
  Goal of ty
  | Undo
  | Qed
  | Check

type instr =
  Cmd of cmd
  | Tact of tactic

type parser_entry =
  | Lam of lam
  | Instr of instr list
Add interactive proofs 2024-04-30 11:44:28 +02:00			`open Lam`
			`open Types`
			`open Proof`

			`type cmd =`
renommage des tactiques, implémentation de la tactique try, suppression des tokens inutiles, etc.. 2024-05-17 14:14:28 +02:00			`Goal of ty`
Add Undo command 2024-05-11 11:44:43 +02:00			`\| Undo`
Add `Qed.` 2024-05-13 18:05:28 +02:00			`\| Qed`
implémentation de la tactique Check pour envoyer la preuve à Coq 2024-05-17 21:28:02 +02:00			`\| Check`
renommage des tactiques, implémentation de la tactique try, suppression des tokens inutiles, etc.. 2024-05-17 14:14:28 +02:00
			`type instr =`
			`Cmd of cmd`
Add interactive proofs 2024-04-30 11:44:28 +02:00			`\| Tact of tactic`

			`type parser_entry =`
			`\| Lam of lam`
renommage des tactiques, implémentation de la tactique try, suppression des tokens inutiles, etc.. 2024-05-17 14:14:28 +02:00			`\| Instr of instr list`