jsiek / deduce

A proof checker meant for education. Primarily for teaching proofs of correctness of functional programs.
59 stars 3 forks source link

Update introduction md files to include list syntax #21

Closed mateidragony closed 1 month ago

mateidragony commented 1 month ago

What's the point of adding a new feature if users don't know about it 😃!

I went ahead and added a section in FunctionalProgramming.md that explains the List syntax sugar right after it explains the Nat syntax sugar.

I also updated some of the code snippets to use the updated list syntax. This we can decide to keep or remove based off of our own preference. I thought it would be nice to have some examples of using the easier syntax, but we may want to keep the empty and node(x, node(y, ...)) syntax in some places.

Another important thing that I updated was the deduce output snippets. This is important because deduce will never (hopefully if I caught everything) output empty or node(x, ...). It should always output [] and [x, ...] and I made it so that the docs reflect that as well.

jsiek commented 1 month ago

Great, thank you!