diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-04 22:17:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:05 +0100 |
| commit | e7c38a5516246b751b89535594075f6f95a243fd (patch) | |
| tree | d48c0510705e7e2207998d6b2d77d30c5076a60d /doc/common | |
| parent | 650ed1278160c2d6dae7914703c8755ab54e095c (diff) | |
RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a local
context for discharge in global declarations. Discharge now done on a
global declaration. Hence removed Def and Assum which were only
partially used (e.g. in rules Def and Assum but not in
delta-conversion, nor in rule Const).
Added discharge rule over definitions using let-in. It replaces the
"substitution" rule since about 7.0.
Diffstat (limited to 'doc/common')
| -rw-r--r-- | doc/common/macros.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 573c3c812..f785a85bb 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -412,6 +412,7 @@ \newcommand{\Fix}[2]{\mbox{\tt Fix}~#1\{#2\}} \newcommand{\CoFix}[2]{\mbox{\tt CoFix}~#1\{#2\}} \newcommand{\With}[2]{\mbox{\tt ~with~}} +\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\substs}[4]{#1\{(#2/#3)_{#4}\}} \newcommand{\Sort}{\mbox{$\cal S$}} |