[xmonad] StackSet patch

[Don Stewart]

Excellent. Applied!

Let us know if you need any help.

wouter:
>
> I found a really minor bug in the "new" function in StackSet.hs. I've  
> attached a patch to fix it.
>
> More interesting, however, is how I found this. I've been transcribing  
> XMonad's StackSets to the functional language/proof assistant Coq. I've 
> set up a darcs repository with my work so far:
>
>   darcs get www.cs.nott.ac.uk/~wss/repos/StackSet
>
> At the moment I have a fairly complete implementation of StackSets in  
> Coq. I have to admit that I did cut a few corners here and there, but  
> there's nothing that can't be fixed with a bit more work. From this Coq 
> file, you can (in principle) extract Haskell code that is pretty close to 
> the current StackSet.hs.
>
> I should emphasize that I haven't proven much about StackSets just yet. 
> This only shows that the definitions in StackSet.hs can be made total 
> (i.e. non-crashing and terminating) in a richer type theory. It should be 
> fun to prove some QuickCheck properties in Coq – which is what I'd like 
> to do next.
>
>   Wouter

> _______________________________________________
> xmonad mailing list
> xmonad at haskell.org
> http://www.haskell.org/mailman/listinfo/xmonad