CODEWITHSUNDEEP
agda
Răzvan Flavius Panda
Răzvan Flavius Panda

Reputation: 22116

Figuring out all functions parameter pattern matches

Having:

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

data One : Bin → Set where
  one : One (x1 nil)
  y0_ : ∀ {bin : Bin} → One bin → One (x0 bin)
  y1_ : ∀ {bin : Bin} → One bin → One (x1 bin)

one-ident : ∀ {x : Bin} → One x → to (from x) ≡ x

What is the logic that generates all the functions parameter pattern matches?

one-ident one = {!   !}
one-ident {x0 x} (y0 o) = {!   !}
one-ident {x1 x} (y1 o) = {!   !}

For example knowing the first argument is {x0 x} why does the 2nd argument have to be (y0 o)? Why can't 2nd argument be (y1 o)?

The code example was taken from here.

Upvotes: 2

Views: 57

Answers (1)

ase
ase

Reputation: 13471

one-ident : ∀ {x : Bin} → One x → to (from x) ≡ x
one-ident one = {!   !}
one-ident {x0 xx} (y0 o) = {!   !}
one-ident {x1 xx} (y1 o) = {!   !}

When you know that x is x0 xx in one-ident you know that the type of the second argument is One (x0 xx). There is only 1 constructor in One that can have that type, namely y0_.

Upvotes: 3

Related Questions