Euclides' grootste gemene deler algoritme GGD

• Coq broncode euclidwrap.v voor GGD
  
  • constructief bewijs van het bestaan van de grootste gemene deler van twee positieve gehele getallen
  • coqqen van de (volledige) file levert een ggd programma (de witness voor het eerste onderdeel)
• Haskell functioneel programma Ggd.hs gegenereerd als in het vorige onderdeel, na selectie van Haskell als Extraction Language
  (Haskell extractie beschikbaar vanaf Coq 7.2)
• Haskell functioneel testprogramma Test.hs . Wrapper voor Ggd.hs
  (gebruikt om de Nat s van Coq te relateren aan de Int s van Haskell).
  Voorbeeld van gebruik:

  prompt> hugs Test 
  __   __ __  __  ____   ___      _________________________________________
  ||   || ||  || ||  || ||__      Hugs 98: Based on the Haskell 98 standard
  ||___|| ||__|| ||__||  __||     Copyright (c) 1994-1999
  ||---||         ___||           World Wide Web: http://haskell.org/hugs
  ||   ||                         Report bugs to: hugs-bugs@haskell.org
  ||   || Version: February 2000  _________________________________________
  
  Haskell 98 mode: Restart with command line option -98 to enable extensions
  
  Reading file "/phil/tf/share/hugs/lib/Prelude.hs":
  Reading file "Test.hs":
  Reading file "Ggd.hs":
  Reading file "Test.hs":
                     
  Hugs session for:
  /phil/tf/share/hugs/lib/Prelude.hs
  Ggd.hs
  Test.hs
  Type :? for help
  Test> ggd 3456 7653
  3
  Test> :q
  [Leaving Hugs]