plfa-exercise

This repo is KAAAsS's exercise of book PLFA.

Generally, all codes in this repo is written by Atom with its plugin agda-mode.

Progress

Part I

• Naturals
• Induction
• Relations
• Equality
• Isomorphism
• Connectives
• Negation
• Quantifiers
• Decidable
• Lists

Part II (In progress)

• Lambda
• Properties
• DeBruijn
• More
• Bisimulation
• Inference
• Untyped