How "with" keyword works in agda ?? and also the code below ??

Question

I am not able to understand it clearly. I tried to learn "with" keyword but there also i have doubt. Please help !!!

I wanted to understand the working of "with" and working of this code.

something-even : ∀ n → Even n ⊎ Even (suc n)
something-even zero = inj₁ zero
something-even (suc n) with something-even n
... | inj₁ x = inj₂ (suc-suc x)
... | inj₂ y = inj₁ y
(this states that either n is even or its successor is even). In fact, thm0 can be implemented without using recursion!

thm0 : ∀ x → ∃ λ y → Even y × x less-than y
thm0 n with something-even n
... | inj₁ x = suc (suc n) , suc-suc x , suc ref
... | inj₂ y = suc n , y , ref

Answer 1

If you are familiar with Haskell, you will notice that in Agda there are no if-statements and no case.

with does pattern-matching of the expression result. For example, with something-even n evaluates something-even n, and then pattern-matches on the following lines with ... | inj₁ x and ... | inj₂ y. These match the expression, to see if its value is constructed using inj₁ or inj₂ constructor, so that the value wrapped by them can be used in the right-hand-side expressions: suc (suc n) , suc-suc x , suc ref uses x determined by inj₁ x, and suc n , y , ref uses y determined by inj₂ y

The actual constructor names come from the definition of ⊎ - see the type of something-even joins types Even n and Even (suc n). So x in inj₁ x corresponds to a value of type Even n for given n, and y in inj₂ y corresponds to a value of type Even (suc n) for the same n.