Parsing.SyntaxSourceParser-level abstract syntax.
Representation of a (located) identifier.
notin id idopts checks that id does not occur in idopts.
are_distinct idopts checks that the elements of idopts of the form Some _ are pairwise distinct.
Identifier of a metavariable.
Representation of a module name.
Representation of a possibly qualified (and located) identifier.
Parser-level (located) term representation.
and p_term_aux = | P_TypeTYPE constant.
*)| P_Iden of p_qident * boolIdentifier. The boolean indicates whether the identifier is prefixed by "@".
*)| P_WildUnderscore.
*)| P_Meta of p_meta_ident * p_term arrayMeta-variable with explicit substitution.
*)| P_Patt of p_ident option * p_term array optionPattern.
*)| P_Appl of p_term * p_termApplication.
*)| P_Arro of p_term * p_termArrow.
*)| P_Abst of p_params list * p_termAbstraction.
*)| P_Prod of p_params list * p_termProduct.
*)| P_LLet of p_ident * p_params list * p_term option * p_term * p_termLet.
*)| P_NLit of intNatural number literal.
*)| P_Wrap of p_termTerm between parentheses.
*)| P_Expl of p_termTerm between curly brackets.
*)Parser-level representation of a function argument. The boolean is true if the argument is marked as implicit (i.e., between curly braces).
nb_params ps returns the number of parameters in a list of parameters ps.
get_impl_params_list l gives the implicitness of l.
p_get_args t is like Core.Term.get_args but on syntax-level terms.
Parser-level inductive type representation.
Rewrite patterns as in Coq/SSReflect. See "A Small Scale Reflection Extension for the Coq system", by Georges Gonthier, Assia Mahboubi and Enrico Tassi, INRIA Research Report 6455, 2016,
Parser-level representation of an assertion.
type p_query_aux = | P_query_verbose of intSets the verbosity level.
*)| P_query_debug of bool * stringToggles logging functions described by string according to boolean.
*)| P_query_flag of string * boolSets the boolean flag registered under the given name (if any).
*)| P_query_assert of bool * p_assertionAssertion (must fail if boolean is true).
| P_query_infer of p_term * Core.Eval.stratType inference command.
*)| P_query_normalize of p_term * Core.Eval.stratNormalisation command.
*)| P_query_prover of stringSet the prover to use inside a proof.
*)| P_query_prover_timeout of intSet the timeout of the prover (in seconds).
*)| P_query_print of p_qident optionPrint information about a symbol or the current goals.
*)| P_query_prooftermPrint the current proof term (possibly containing open goals).
*)Parser-level representation of a query command.
type p_tactic_aux = | P_tac_admit| P_tac_apply of p_term| P_tac_assume of p_ident option list| P_tac_fail| P_tac_generalize of p_ident| P_tac_have of p_ident * p_term| P_tac_induction| P_tac_query of p_query| P_tac_refine of p_term| P_tac_refl| P_tac_rewrite of bool * p_rw_patt option * p_term| P_tac_simpl of p_qident option| P_tac_solve| P_tac_sym| P_tac_why3 of string optionParser-level representation of a tactic.
is_destructive t says whether tactic t changes the current goal.
Parser-level representation of a proof.
type p_modifier_aux = | P_mstrat of Core.Term.match_stratpattern matching strategy
*)| P_expo of Core.Term.expovisibility of symbol outside its modules
*)| P_prop of Core.Term.propsymbol properties: constant, definable, ...
*)| P_opaqopacity
*)Parser-level representation of modifiers.
type p_symbol = {p_sym_mod : p_modifier list;modifiers
*)p_sym_nam : p_ident;symbol name
*)p_sym_arg : p_params list;arguments before ":"
*)p_sym_typ : p_term option;symbol type
*)p_sym_trm : p_term option;symbol definition
*)p_sym_prf : (p_proof * p_proof_end) option;proof script
*)p_sym_def : bool;is it a definition ?
*)}Parser-level representation of symbol declarations.
type p_command_aux = | P_require of bool * p_path list| P_require_as of p_path * p_ident| P_open of p_path list| P_symbol of p_symbol| P_rules of p_rule list| P_inductive of p_modifier list * p_params list * p_inductive list| P_builtin of string * p_qident| P_notation of p_qident * Core.Sign.notation| P_unif_rule of p_rule| P_query of p_queryParser-level representation of a single command.
Parser-level representation of a single (located) command.
Equality functions on the syntactic expressions ignoring positions.
eq_command c1 c2 tells whether c1 and c2 are the same commands. They are compared up to source code positions.
fold_proof f acc p recursively builds a value of type 'a by starting from acc and by applying f to every tactic of p.
fold_idents f a ast allows to recursively build a value of type 'a starting from a and by applying f on each identifier occurring in ast corresponding to a function symbol: variables (term variables or assumption names) are excluded.
NOTE: This function is incomplete if an assumption name hides a function symbol. Example:
symbol A:TYPE; symbol a:A; symbol p:((A->A)->A->A)->A := begin assume h apply h // proof of A->A assume a apply a // here a is an assumption // proof of A apply a // here a is a function symbol end;