From cee37c7a5aa40d1b6d978a5e1aa3a2d91cdb7a63 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 6 Mar 2012 12:11:14 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter9.ma | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma index a5dfd1c98..b3f46ae04 100644 --- a/weblib/tutorial/chapter9.ma +++ b/weblib/tutorial/chapter9.ma @@ -1,7 +1,15 @@ (* -h1Moves/h1*) +h1Moves/h1We now define the move operation, that corresponds to the advancement of the +state in response to the processing of an input character a. The intuition is +clear: we have to look at points inside $e$ preceding the given character a, +let the point traverse the character, and broadcast it. All other points must +be removed. + +We can give a particularly elegant definition in terms of the +lifted operators of the previous section: +*) -include "chapter8.ma". +include "tutorial/chapter8.ma". let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝ match E with -- 2.39.2