Due by Thu, 24 Jan 2019
Please e-mail your assignments to email@example.com with "LTS2019" in the subject. The submissions will be added to the repository the day after the due date, and no late submissions will be accepted.
All problems should be solved in an
Idris file which should be in a folder including the files
Evens.idr from the course. If your user name is firstname.lastname@example.org, begin the idris file with the following.
module Myusername.Odds import Evens import Intro
IsOdd : Nat -> Typesuch that
IsOdd nis inhabited if and only if
$2$is not odd.
n: Natis odd, then its successor
S nis even.
n: Natis even, then its successor
S nis odd.
n : Natis either even or odd.
n: Natis both even and odd.
m: Natare odd, then
add n mis even (here add is from the intro).
n: Natis odd, then there exists
m: Natsuch that
n = S (double m).