core-to-isabelle

core-to-isabelle copied to clipboard

It would be nice to allow users to write QuickCheck properties, use them with QuickCheck at first. Then, once they pass enough random tests, users can attempt to prove that...

atomb

Add an isabelle command like this: halicore_symbol "" "zlzdzg" The first parameter is the name as it appears in the Haskell program and the second parameter is the matching z...

dagit

- Alpha renaming should be a different step - zdecoding should be a different step - simplified pretty printing AST

dagit

Output special isabelle syntax for lists

1

dagit

Add special syntax for lists on the Halicore side

1

dagit

dagit

dagit

dagit

Add support in the translator to catch identifiers that Isabelle cannot parse and output a renaming and a comment to help the programmer see the renaming.

dagit

dagit