package coq-core
On This Page
The Coq Proof Assistant -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/ltac2_plugin/Ltac2_plugin/Tac2quote/index.html
Module Ltac2_plugin.Tac2quoteSource
Syntactic quoting of expressions.
Contrarily to Tac2ffi, which lives on the semantic level, this module manipulates pure syntax of Ltac2. Its main purpose is to write notations.
Source
val constructor :
?loc:Loc.t ->
Tac2expr.ltac_constructor ->
Tac2expr.raw_tacexpr list ->
Tac2expr.raw_tacexprSource
val of_pair :
('a -> Tac2expr.raw_tacexpr) ->
('b -> Tac2expr.raw_tacexpr) ->
('a * 'b) CAst.t ->
Tac2expr.raw_tacexprSource
val of_open_constr :
?delimiters:Names.Id.t list ->
Constrexpr.constr_expr ->
Tac2expr.raw_tacexprSource
val of_preterm :
?delimiters:Names.Id.t list ->
Constrexpr.constr_expr ->
Tac2expr.raw_tacexprid ↦ 'Control.hyp @id'
id ↦ 'Control.refine (fun () => Control.hyp @id')
id ↦ 'Control.refine (fun () => Control.hyp @id')
Generic arguments
Source
val wit_pattern :
(Constrexpr.constr_expr, [ `uninstantiated ] Pattern.constr_pattern_r)
Tac2dyn.Arg.tagSource
val wit_preterm :
(Constrexpr.constr_expr, Names.Id.Set.t * Glob_term.glob_constr)
Tac2dyn.Arg.tagSource
val wit_ltac1 :
(Names.Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr,
Names.Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr)
Tac2dyn.Arg.tagLtac1 AST quotation, seen as a 'tactic'. Its type is unit in Ltac2.
Source
val wit_ltac1val :
(Names.Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr,
Names.Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr)
Tac2dyn.Arg.tagLtac1 AST quotation, seen as a value-returning expression, with type Ltac1.t.
On This Page