X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fastfe_tree.ma;h=626248685c758df6a297f36644b091ee913861c1;hb=759451f66c0009b12e5bcc9fe0c61f7ab5277057;hp=2690b2466f8e85895d50f9a0b2574bcf8933a552;hpb=5688b80cf330cc66038720e04cf7c0293630c163;p=helm.git diff --git a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma index 2690b2466..626248685 100755 --- a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma +++ b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma @@ -57,6 +57,12 @@ inductive astfe_expr (e:aux_flatEnv_type) : ast_type → Type ≝ astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_SHL: ∀t:ast_base_type. astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_AND: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_OR: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_XOR: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_GT : ∀t:ast_base_type. astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)