From 21327e3d4257eb77e8b8470dea00ad99ffcd85b0 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Thu, 1 Jul 2021 14:03:16 +0200 Subject: [PATCH] explain in beginning of chap1, that all snippets have to be executed in order explain when using the big operation that we are re-using a notation --- tex/chProgramming.tex | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/tex/chProgramming.tex b/tex/chProgramming.tex index c422aa25..6cbdf50b 100644 --- a/tex/chProgramming.tex +++ b/tex/chProgramming.tex @@ -22,6 +22,12 @@ \chapter{Functions and computation}\label{ch:prog} % \Coq{}, how to perform computations and how to define basic % mathematical objects. +This chapter provides code snippets that can be loaded in a Coq session, +after the header described at the the end of the introduction chapter. +These snippets should be loaded in order and without +omission to avoid mistakes that would take too long to explain +at this introductory level. + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Functions}\label{sec:functions} Before being more @@ -2182,10 +2188,13 @@ \section{Iterators and mathematical notations} The \C{iota} function generates the list \C{[:: m; m+1; ...; m+n-1]} of natural numbers -corresponding to the range of the summation. Then the notation defines -expressions with shape \C{\\sum\_ (m <= i < n) F}, with \C{F} a +corresponding to the range of the summation. +On the second line, we re-use a notation that is already present in +the library with shape \C{\\sum\_ (m <= i < n) F}, with \C{F} a sub-expression featuring variable \C{i}, the one used for the -index. For instance, once the above notation is granted and for any +index. We attach this notation to a specific expression combining +\C{foldr} and \C{iota}. +For instance, once the above notation is granted and for any natural number \C{(n : nat)}, one may write the \Coq{} expression \C{(\\sum\_(1 <= i < n) i)} to represent the sum $\sum\limits_{i=1}^{n-1} i$. The name \C{i} is really used as a