Align types in even and odd example

This commit is contained in:
Matthew Healy 2020-07-16 18:31:16 +02:00
parent 697174cd47
commit 2a620487f6

View file

@ -661,7 +661,7 @@ data even where
data odd where data odd where
suc : ∀ {n : } suc : ∀ {n : }
→ even n → even n
----------- -----------
→ odd (suc n) → odd (suc n)