leanprover-community
Add whilecc.lean
Hello,
I translated a parts of the correctness proof for the compiler in the Concrete Semantics book into Lean and thought it could be useful for other people. I know that it doesn't fully comply with the mathlib style and some definitions are redundant with definitions in mathlib proper. A while ago I tried using the proper mathlib definitions (specifically relation.trans_gen) but I failed. I can't exactly remember what went wrong, but I though that this would still be useful so I'm submitting this pull request anyways.
If somebody wants to fix the code to comply with the mathlib style, please feel free to do so. See #10315 for comments from previous reviewers.
@Zetagon can you please add a copyright header, in case someone wants to pick this up?
@Ruben-VandeVelde I've added copyright notices and some comments for the parts that were copied from The Hitchhiker's Guide. Not sure if that's enough though.