Stream: math-comp users

Topic: Order of multiple views in apply


view this post on Zulip Alexander Gryzlov (Jun 17 2021 at 14:54):

Suppose I have something like

Parameter X Y Z: Set.
Axiom foo : X -> Y -> Z.
Axiom x : X.
Axiom y : Y.

Lemma test : Z.
Proof.
apply/foo/y/x.
Qed.

Why do chained apply views work on the last generated goal rather than the top one, i.e. the proof above works but apply/foo/x/y doesn't?


Last updated: Feb 08 2023 at 07:02 UTC