Conversation
fblanqui
left a comment
fblanqui
left a comment
There was a problem hiding this comment.
Thanks Jean-Paul for your PR. Here are my comments:
| begin | ||
| assume T a b h1 h2; | ||
| first_hyp (λ _ _ ph, #apply ph); | ||
| debug +t; |
| assume T a b h1 h2; | ||
| first_hyp (λ _ _ ph, #apply ph); | ||
| debug +t; | ||
| first_hyp (λ l (v: U l) (ph: η v), #apply ph); |
There was a problem hiding this comment.
are type annotations necessary?
There was a problem hiding this comment.
yes and this is why I declared #first_hyp parameters mandatory in Tactic.lp even it concerns first_hyp.
There was a problem hiding this comment.
why are type annotations necessary?
| builtin "fail" ≔ #fail; | ||
|
|
||
| constant symbol #first_hyp: (Π [l] [a:U l], η a → Tactic) → Tactic; | ||
| constant symbol #first_hyp: (Π l (a:U l), η a → Tactic) → Tactic; |
There was a problem hiding this comment.
Why l is not declared as implicit?
There was a problem hiding this comment.
to recall they are mandatory in first_hyp (without the '#').
| of underlining the whole command or tactic (symbol body, rule right-hand | ||
| side, proof, etc.). | ||
| - Tactics first_hyp and all_hyps made compatible with \eta signatures. | ||
| Tactic first_hyp considers #nothing has a success. |
There was a problem hiding this comment.
No need to add anything in CHANGES (CHANGES record main changes wrt the previous release, not the commit history).
| let p = new_problem() in | ||
| let ml = mk_Meta(LibMeta.fresh p (Env.to_prod env mk_Level) n,args) in | ||
| let mt = mk_Meta(LibMeta.fresh p (Env.to_prod env (mk_univ ml)) n,args) in | ||
| let t = mk_Appl(mk_Appl(mk_Appl(t,ml),mt),mk_Vari v) in |
There was a problem hiding this comment.
You can use add_args instead if you want.
| begin | ||
| assume T a b c h1 h2; | ||
| all_hyps (λ _ h ph, #rewrite "" "" ph); | ||
| all_hyps (λ l (h:U l) (ph: η h), #rewrite "" "" ph); |
There was a problem hiding this comment.
Are type annotations necessary?
| @@ -1,17 +1,16 @@ | |||
| require open tests.OK.Tactic; | |||
| require open tests.OK.Prop tests.OK.Set tests.OK.Univ tests.OK.Tactic; | |||
There was a problem hiding this comment.
Please minimize the number of required files.
| begin | ||
| assume T a b h1 h2; | ||
| eval #first_hyp (λ _ _ ph, #apply ph); | ||
| eval (#first_hyp (λ l (v: U l) ph, #apply ph)); |
There was a problem hiding this comment.
Are type annotations and outer parentheses necessary?
There was a problem hiding this comment.
OK type annotations are useless in #first_hyp
| let check id = | ||
| if Env.mem id.elt env then fatal id.pos "Identifier already in use." in | ||
| (* tries to apply tactic t on context variable v *) | ||
| let apply_context ps c g v t = |
There was a problem hiding this comment.
The name does not really correspond to the comment. What about apply_hyp?
I would also precise in the comment that t is a tactic term.
The function apply_hyp is iterated many times but many let's below are identical in each call. It would be better to compute them only once. The let's below should be done before calling the function and passed as arguments. This creates some duplication in the code below but that's ok I think.
In the end, we would get:
(* tries to apply tactic term t on context variable v *)
let apply_hyp ps g c t v level univ n args = ...
where:
let level = mk_Symb(Builtin.get ss pos [] "Level") in
let univ = mk_Symb(Builtin.get ss pos [] "Univ") in
let n = List.length env in
let args = Env.to_terms env in
2 participants
This patch fixes errors linked to the \eta profiles and allows tactics without side effects to be considered as successful by first_hyp.