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.

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: Jul 23 2024 at 21:01 UTC