module Rewrite:sig
..end
setoid_rewrite
type
hypinfo = {
|
hyp : |
(* | the actual constr corresponding to the hypothese | *) |
|
hyptype : |
(* | the type of the hypothesis | *) |
|
context : |
(* | the quantifications of the hypothese | *) |
|
body : |
(* | the body of the hypothese | *) |
|
rel : |
(* | the relation | *) |
|
left : |
(* | left hand side | *) |
|
right : |
(* | right hand side | *) |
|
l2r : |
(* | rewriting from left to right | *) |
typeof hyp = typ
typ = forall context, body
body = rel left right
val get_hypinfo : Term.constr ->
l2r:bool ->
?check_type:(Term.types -> bool) ->
(hypinfo -> Proof_type.tactic) -> Proof_type.tactic
get_hypinfo H l2r ?check_type k
analyse the hypothesis H, and
build the related hypinfo, in CPS style. Moreover, an optionnal
function can be provided to check the type of every free
variable of the body of the hypothesis.
The problem : Given a term to rewrite of type H :forall xn ... x1,
t
, we have to instanciate the subset of xi
of type
carrier
. subst : (int * constr)
is the mapping the De Bruijn
indices in t
to the constrs
. We need to handle the rest of the
indexes. Two ways :
H tn ?1 tn-2 ?2
fun 1 2 => H tn 1 tn-2 2
val build : hypinfo ->
(int * Term.constr) list ->
(Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val build_with_evar : hypinfo ->
(int * Term.constr) list ->
(Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val rewrite : ?abort:bool ->
hypinfo ->
(int * Term.constr) list ->
(Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic
rewrite ?abort hypinfo subst
builds the rewriting tactic
associated with the given subst
and hypinfo
, and feeds it to
the given continuation. If abort
is set to true
, we build
tclIDTAC
instead.