# Syntactic quirks

We capture here some of the caveats and syntactic sugars here.

``````module Lang.syntaxQuirks where

open import Lang.dataStructures
open import Agda.Builtin.Equality``````

# Syntactic sugars

Mostly short-forms of various stuff used more often.

## Common parameters

The implicit parameter `{m : ℕ}` common to all constructors can be abstracted out into the data definition:

``````data _≤′_ : ℕ → ℕ → Set where
≤′-refl : {m : ℕ} →                       m ≤′ m
≤′-step : {m : ℕ} → {n : ℕ} →  m ≤′ n  →  m ≤′ succ n``````

is same as

``````data _≤′₁_ (m : ℕ) : ℕ → Set where
≤′₁-refl :                       m ≤′₁ m
≤′₁-step : {n : ℕ} →  m ≤′₁ n  →  m ≤′₁ succ n``````

## Different ways of defining `data`

The previous technique also works for concrete parameters:

``````data _≤″_ : ℕ → ℕ → Set where
≤″ : ∀ {m n k} → m + n ≡ k → m ≤″ k``````

is same as

``````data _≤″₁_ (m : ℕ) : ℕ → Set where
≤+ : ∀ {n k} → m + n ≡ k → m ≤″₁ k``````

which is same as

``````data _≤″₂_ (m : ℕ) (k : ℕ) : Set where
≤+ : ∀ {n} → m + n ≡ k → m ≤″₂ k``````

## Implicit arguments

Arguments that can be inferred by the compiler can be left out with an `_`:

``````length : (A : Set) (len : ℕ) → Vec A len → ℕ
length A zero [] = zero
length A len somevec = len``````
``````length' : (A : Set) (len : ℕ) → Vec A len → ℕ
length' A zero [] = zero
length' A len _   = len``````
``````length'' : (A : Set) (len : ℕ) → Vec A len → ℕ
length'' A zero [] = zero
length'' _ len _   = len``````

Though these are generally ill-advised as they may cause confusion when used unwisely.

Debugging