Ssreflect Users Discussion List

[Mitchell Wand <>]

Ahh, thank you.  That is very useful.  

I am impressed that the index is so short.  That means fewer things for me to memorize :)

On the other hand, I find the long chains of tacticals difficult to understand.  For example, in

elim=> [|m IHm] [|n] //; exact: IHm. 

what is the [|n] doing?  Is there a general technique for breaking down a complicated tactical into a series of commands so I can see what each tactical is doing? For example,I canreplace the ";" by a "." and then examine the individual subgoals, but I don't know how to do this in general.

Sorry if this question marks me as a newbie.

--Mitch

On Mon, Feb 12, 2018 at 10:21 AM, Enrico Tassi <> wrote:

On Sat, Feb 10, 2018 at 09:33:15AM -0500, Mitchell Wand wrote:
> ​Can anybody tell me where to find the solutions to "An introduction to
> small scale reflection​ in Coq"?
>
> The paper promises solutions at
> www.msr-inria.inria.fr/Projects/math-components, but I couldn't find them.

Dear Mitch, I found the solutions (in attachment).

I would also like to point out that, if you are looking for an
introduction to ssr/math-comp you may also want to take a look at
the book draft: https://math-comp.github.io/mcb/

Best
--
Enrico Tassi