search

isovector / certainty-by-construction

Source material for Certainty by Construction
https://leanpub.com/certainty-by-construction/
36 stars 9 forks source link

Certainty by Construction PDF page 25 MakeCase #2

Closed onelinelernen closed 1 year ago

onelinelernen commented 1 year ago

What is "agda:MakeCase" or better "MakeCase" ?

I'm typing along the book in vs code and I'm completely stuck on page 25

Position your cursor on the hole and invoke the agda:MakeCase , which will replace our definition with:

Things like "module" and

open Data.Bool : Bool = false

work just fine in agda / vs code on my windows PC with wsl2, but no idea how to use or make sense of the (command ?) "MakeCase"

isovector commented 1 year ago

Hi, thanks for reaching out!

agda:MakeCase is an annotation in the book I haven't successfully pretty-printed yet. It means to press Ctrl-C + Ctrl-C (to invoke "case split" as documented here). You might need to hit enter again afterwards to make progress.

Sometimes I'll write MakeCase:x to suggest that you should press Ctrl-C + Ctrl-C, and then type x into the pop-up prompt.

onelinelernen commented 1 year ago

thank you for your answer - it works !

isovector commented 1 year ago

I've fixed this in the source material, and Friday's update will dramatically clean up the typesetting involved here. Thanks for reporting this!