From 5372de545efe718a5ea3fcae8996da22d39cc360 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 9 Dec 2004 15:18:50 +0000 Subject: [PATCH] addded inductive definition to AST --- helm/ocaml/cic_transformations/tacticAst.ml | 6 ++++++ helm/ocaml/cic_transformations/tacticAstPp.ml | 1 + 2 files changed, 7 insertions(+) diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 112d87b70..28b256c86 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -84,6 +84,10 @@ type thm_flavour = | `Theorem ] + (** + * true means inductive, false coinductive *) +type 'term inductive_type = string * bool * 'term * (string * 'term) list + type 'term command = | Abort | Baseuri of string option (** get/set base uri *) @@ -94,6 +98,8 @@ type 'term command = * Name is needed when theorem was started without providing a name *) | Quit + | Inductive of (string * 'term) list * 'term inductive_type list + (** parameters, list of mutual inductive types *) | Theorem of thm_flavour * string option * 'term * 'term option (** flavour, name, type, body * - name is absent when an unnamed theorem is being proved, tipically in diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index d0e87b094..32f7ace8e 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -107,6 +107,7 @@ let pp_command = function | Quit -> "Quit" | Redo None -> "Redo" | Redo (Some n) -> sprintf "Redo %d" n + | Inductive _ -> (* TODO Zack *) assert false | Theorem (flavour, name, typ, body) -> sprintf "%s %s: %s %s" (pp_flavour flavour) -- 2.39.2