Contents Previous Next

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