]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/assembly/compiler/astfe_tree.ma
mod change (-x)
[helm.git] / helm / software / matita / contribs / assembly / compiler / astfe_tree.ma
old mode 100755 (executable)
new mode 100644 (file)
index 2690b24..6262486
@@ -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)