Related for people into provers, there is a set of notes here https://cs.uwaterloo.ca/~plragde/842/handouts/notes.html https://cs.uwaterloo.ca/~plragde/842/hand

Related for people into provers, there is a set of notes here https://cs.uwaterloo.ca/~plragde/842/handouts/notes.html https://cs.uwaterloo.ca/~plragde/842/handouts/notes.html to help you work through the Agda book https://plfa.github.io/ https://plfa.github.io/ which is done using emacs, atom or vscode