From 11f0f9739cdec05a1058e3492968ecead0be48f0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Sep 2009 11:11:34 +0000 Subject: [PATCH] some work --- .../contribs/ng_assembly/compiler/preast_tree.ma | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma b/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma index 5263b84e4..27fbbb72c 100755 --- a/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma +++ b/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma @@ -73,7 +73,7 @@ with preast_var : Type ≝ (* -------------------------- *) (* inizializzatori: ... valori ... *) -inductive preast_init_val : Type ≝ +ninductive preast_init_val : Type ≝ PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val | PREAST_INIT_VAL_WORD16: word16 → preast_init_val | PREAST_INIT_VAL_WORD32: word32 → preast_init_val @@ -85,17 +85,17 @@ inductive preast_init_val : Type ≝ 1) var1 = var2 2) var = ... valori ... *) -inductive preast_init : Type ≝ +ninductive preast_init : Type ≝ PREAST_INIT_VAR: preast_var → preast_init | PREAST_INIT_VAL: preast_init_val → preast_init. (* -------------------------- *) (* statement: assegnamento/while/if else if else *) -inductive preast_stm : Type ≝ +ninductive preast_stm : Type ≝ PREAST_STM_ASG: preast_var → preast_expr → preast_stm | PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm -| PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm +| PREAST_STM_IF: ne_list (ProdT preast_expr preast_decl) → option preast_decl → preast_stm (* dichiarazioni *) with preast_decl : Type ≝ @@ -106,10 +106,10 @@ with preast_decl : Type ≝ (* -------------------------- *) (* programma *) -inductive preast_root : Type ≝ +ninductive preast_root : Type ≝ PREAST_ROOT: preast_decl → preast_root. (* -------------------------- *) (* programma vuoto *) -definition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)). +ndefinition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)). -- 2.39.2