Due by Thu, 24 Jan 2019

Please e-mail your assignments to siddhartha.gadgil@gmail.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 `Intro.idr`

and `Evens.idr`

from the course. If your user name is *myusername@iisc.ac.in*, begin the idris file with the following.

```
module Myusername.Odds
import Evens
import Intro
```

- Define an inductive type family
`IsOdd : Nat -> Type`

such that`IsOdd n`

is inhabited if and only if`n`

is odd. - Show that
`$3$`

is odd. - Show that
`$2$`

is not odd. - Show that if
`n: Nat`

is odd, then its successor`S n`

is even. - Show that if
`n: Nat`

is even, then its successor`S n`

is odd. - Show that every number
`n : Nat`

is either even or odd. - Show that no number
`n: Nat`

is both even and odd. - Show that if
`n: Nat`

and`m: Nat`

are odd, then`add n m`

is even (here add is from the intro). - Show that if
`n: Nat`

is odd, then there exists`m: Nat`

such that`n = S (double m)`

.