§ Agda Cheat Sheet

• Load/check file: C-c C-l.
• Show goals: C-c C-?.
• Accept goal value: C-c C-SPACE
• forward goal: C-c C-f
• backward goal: C-c C-b
• Normal form: C-c C-n
• see how to write symbol: M-x quail-show-key.
• Within goal: Case split: C-c C-c.
• Within goal: Refine: C-c C-r. Partial give: makes new holes for missing arguments
• Within goal: Type: C-c C-t.
• Within goal: Deduce type: C-c C-d.
• Within goal: Information: C-c C-;.