From 47079f99d6e48c735dec6b30f47a5f8c238bdab5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 29 Aug 2014 16:02:03 +0000 Subject: [PATCH] Notes. --- matita/matita/lib/tutorial/chapter12.ma | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/matita/matita/lib/tutorial/chapter12.ma b/matita/matita/lib/tutorial/chapter12.ma index 7923b2b26..c0d8f8ae8 100644 --- a/matita/matita/lib/tutorial/chapter12.ma +++ b/matita/matita/lib/tutorial/chapter12.ma @@ -631,6 +631,15 @@ theorem div_trace_to_diverging_trace': | #n #s #EQ destruct lapply (div_well_formed d n) /2 by div_well_formed, next_step/ ] qed. +(* AGGIUNGERE SPIEGAZIONE SU PRODUTTIVITA' *) + +(* AGGIUNGERE SPIEGAZIONE SU CONFRONTO VALORI COINDUTTIVI *) + +(* AGGIUNGERE CONFRONTO CON TEORIA DELLE CATEGORIE *) + +(* AGGIUNGERE ESEMPI DI SEMANTICA OPERAZIONE BIG STEP PER LA DIVERGENZA; + DI PROPRIETA' DI SAFETY; + DI TOPOLOGIE COINDUTTIVAMENTE GENERATE? *) (* ################## COME SPIEGARLO QUI? ####################### *) -- 2.39.2