CODEWITHSUNDEEP
coqssreflect
thor
thor

Reputation: 22480

what does the curly braces {} do in ssreflect rewrite

I am reading and playing with a ssreflect tutorial, and encountered a use of {} to quote things, which I don't quite understand:

Variables P Q : bool -> Prop.
Hypothesis P2Q : forall a b, P (a || b) -> Q a.
Goal forall a, P (a || a) -> True.
  move=> a HPa. move: {HPa} (@P2Q _ _ HPa) => HQa.

Can anyone explain what does {HPa} do to HPa?

BTW, the context was to introduce "views"??. I tried removing the {}, it still works but generates something different. And I don't know where to look for documentation for things like brackets or @ for that matter.

Upvotes: 0

Views: 381

Answers (1)

thor
thor

Reputation: 22480

After some experiments and comparison, it seems that the function of {H} is to clear H. in Coq terms.

move: {HPa} (@P2Q _ _ HPa) => HQa.

gives

1 subgoals
a : bool
HQa : Q a
______________________________________(1/1)
True

while 

move: (@P2Q _ _ HPa) => HQa.

gives the same thing except that HPa is kept intact in the context:

1 subgoals
a : bool
HPa : P (a || a)
HQa : Q a
______________________________________(1/1)
True

Upvotes: 1

Related Questions