Re: [isabelle] A (very) short Isabelle/HOL tutorial for the functional programmer



On Mon, Oct 19, 2015 at 7:01 PM, Makarius <makarius at sketis.net> wrote:

> On Mon, 19 Oct 2015, Thomas Genet wrote:
>
> I wrote a 4 pages Isabelle/HOL tutorial for the functional programmer. It
>> is available here:
>>
>> https://hal.inria.fr/hal-01208577v2
>>
>> Any feedback and comments are welcome.
>>
>
>

The text reads a bit like a "script" for an interactive session, conducted
> by the user or the presenter of a quick tutorial. It would be nice to see
> online videos like that.
>
>
When I reach there I'll make one :-) But for now...


For me it is always interesting to see what needs to be explained on first
> encounter.
>
>
Programmers need a "Hello World" example to get off the ground.
Until I saw Thomas' example I could not understand that (or rather how)
Isabelle hops between define-mode (eg fun/primrec etc) and prove-mode
(lemma...apply... etc)



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.