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.


Modules, Records and Postulates