# How do clausal definitions work?

I'm most familiar with the metatheory of calculi based around expressions.

But systems like Agda use separate clauses for definitions.

ifte : { A : Set } -> bool -> A -> A -> A
ifte true x y = x
ifte false x y = y


Copatterns are a similar construct.

I'm mostly interested because I was interested in whether this sort of thing could simplify use of positive types.

For the STLC this sort of scheme suggests an almost ANFish sort of approach?

$$\frac{x \colon \tau \in \Gamma}{\Gamma \vdash x \colon \tau}$$

$$\frac{ \begin{split}\Gamma, x\colon \tau_1 \vdash e_1 \colon \tau_2\\ \Gamma, y\colon \tau_1 \to \tau_2 \vdash e_2\colon \tau_3 \end{split}}{\Gamma \vdash \textbf{let} \, y \, x := e_1 \, \textbf{in} \, e_2 \colon \tau_3}$$

$$\frac{ \begin{split}\Gamma \vdash e_1 \colon \tau_1 \to \tau_2\\ \Gamma \vdash e_2 \colon \tau_1 \end{split}}{\Gamma \vdash e_1 e_2 \colon \tau_2}$$

I think for sum types you might have pattern matching like

$$\frac{ \begin{split} \Gamma, x\colon \tau_1 \vdash e_1 \colon \tau_3\\ \Gamma , x\colon \tau_2 \vdash e_2 \colon \tau_3\\ \Gamma , y\colon \tau_1 + \tau_2 \to \tau_3 \vdash e_3 \colon \tau_4 \end{split}}{\Gamma \vdash \textbf{let} \, \begin{split}y \, x := e_1 \\ y \, x := e_2 \end{split} \, \textbf{in} \, e_3 \colon \tau_3}$$

I'm not really sure I'm getting the spirit of clausal definitions or how they might simplify things.

How precisely would you formalize these sort of clausal definitions?

• I was reminded about clausal definitions here Oct 23 at 21:15

As for how it simplifies stuff, see if you can define head : Vec (suc n) A -> A that fetches the first element of a nonempty vector using eliminators only. (Hint: it's very long.) More in-depth discussion of this can be found at