Mercurial > urweb

comparison doc/manual.tex @ 532:23718a4b23d7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Definitional equality
author Adam Chlipala <adamc@hcoop.net>
date Sat, 29 Nov 2008 10:05:46 -0500
parents e47eff8c9037
children 419f51b1e68d
comparison
equal deleted inserted replaced
531:e47eff8c9037 532:23718a4b23d7
347 } 347 }
348 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{ 348 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
349 \Gamma \vdash c \hookrightarrow C 349 \Gamma \vdash c \hookrightarrow C
350 }$$ 350 }$$
351 351
352 \subsection{Definitional Equality}
353
354 We use $\mathcal C$ to stand for a one-hole context that, when filled, yields a constructor. The notation $\mathcal C[c]$ plugs $c$ into $\mathcal C$. We omit the standard definition of one-hole contexts. We write $[x \mapsto c_1]c_2$ for capture-avoiding substitution of $c_1$ for $x$ in $c_2$.
355
356 $$\infer{\Gamma \vdash c \equiv c}{}
357 \quad \infer{\Gamma \vdash c_1 \equiv c_2}{
358 \Gamma \vdash c_2 \equiv c_1
359 }
360 \quad \infer{\Gamma \vdash c_1 \equiv c_3}{
361 \Gamma \vdash c_1 \equiv c_2
362 & \Gamma \vdash c_2 \equiv c_3
363 }
364 \quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{
365 \Gamma \vdash c_1 \equiv c_2
366 }$$
367
368 $$\infer{\Gamma \vdash x \equiv c}{
369 x :: \kappa = c \in \Gamma
370 }
371 \quad \infer{\Gamma \vdash M.x \equiv c}{
372 \Gamma \vdash M : S
373 & \mt{proj}(M, S, \mt{con} \; x) = (\kappa, c)
374 }
375 \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$
376
377 $$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{}
378 \quad \infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{}
379 \quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$
380
381 $$\infer{\Gamma \vdash [] \rc c \equiv c}{}
382 \quad \infer{\Gamma \vdash [\overline{c_1 = c'_1}] \rc [\overline{c_2 = c'_2}] \equiv [\overline{c_1 = c'_1}, \overline{c_2 = c'_2}]}{}$$
383
384 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c \equiv c}{
385 \Gamma \vdash c_1 \sim c_2
386 }
387 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; [] \equiv i}{}
388 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; ([c_1 = c_2] \rc c) \equiv f \; c_1 \; c_2 \; (\mt{fold} \; f \; i \; c)}{}$$
389
390 $$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{}
391 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; (\mt{map} \; f' \; c)
392 \equiv \mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) \Rightarrow f \; x_1 \; (f' \; x_2)) \; i \; c}{}$$
393
394 $$\infer{\Gamma \vdash \mt{map} \; f \; (c_1 \rc c_2) \equiv \mt{map} \; f \; c_1 \rc \mt{map} \; f \; c_2}{}$$
352 395
353 \end{document} 396 \end{document}