CODEWITHSUNDEEP
coqssreflect
setholopolus
setholopolus

Reputation: 265

Alternative tactic for `ssreflect`'s `move=>`

I like using the move=> tactic from the ssreflect library in cases when the goal is an implication (e.g. A -> B), to make the premise a hypothesis, and make the conclusion the new goal. However, I don't always want to use ssreflect.

Is there another Coq tactic that does the same thing without using ssreflect?

Upvotes: 0

Views: 116

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

You can always use intros: intros pat is roughly equivalent to move=> pat. Unfortunately, Coq and ssreflect use a different syntax for introduction patterns, so the two are not interchangeable.

Note that nowadays ssreflect is part of the Coq distribution, so you can use the tactic language by simply doing From Coq Require Import ssreflect., without the need for installing a separate library.

Upvotes: 3

Related Questions