Re: [isabelle] automatically grade Isabelle homework?

On 07/09/2016 11:53 AM, Lars Hupel wrote:

>> 1. what is the best way to pattern-match
>> student's Isabelle code against problem statement?
>> For Haskell, I actually compare abstract syntax trees.
> is there any reason you require students to exactly fill out holes? 

Well, you can always give a name to a "hole" inside an expression.
Then student has to add a top-level definition for that name.

But then, being top-level (module-level)
means that it cannot refer to local names
from the scope that the hole was in,
but sometimes that's the point of an exercise,
if it's about "local" programming techniques.

Also, there are other kinds of holes (than expressions),
I want to use this also for patterns and types.
Again, these could be named, but then I lose the scope information,
or have to make it explicit (by adding arguments).

I imagine the same could be useful for Isabelle homework:
"fill the gap(s) in this proof (but don't touch the non-gaps)"
the point being that the student has to respect the (local) structure.

- Johannes.

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