This repository contains the topics covered during the Static Analysis and Program Verification (SAPV) course. The repo is written entirely in Agda, It is assumed to use emacs as text editor to make using agda as simple as possible.
| Command | Action |
|---|---|
| C-c | Load the current file |
| C-c C-d expression | Show the type of expression |
| C-c C-n expression | Normalize expression |
| C-c C-c argument | Perform case analysis on argument |
| C-c C-, | Show goal and context |
| C-c C-f | Move forward to the next goal |
| C-c C-b | Move backward to the previous goal |
| C-c C-r | Refine the current hole |
| C-c C-SPACE | Fill the hole with the provided expression |