package coq-core
On This Page
The Coq Proof Assistant -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
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