-
-(* mini test
-definition prova ≝
-PREAST_ROOT (
- PREAST_DECL true [ ch_Q ] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (None ?) (
- PREAST_NO_DECL [
- PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x0,x0〉) (
- PREAST_DECL false [ ch_P ] (AST_TYPE_STRUCT «(AST_TYPE_BASE AST_BASE_TYPE_WORD16)£(AST_TYPE_BASE AST_BASE_TYPE_BYTE8)») (None ?) (
- PREAST_NO_DECL [
- PREAST_STM_ASG (PREAST_VAR_STRUCT (PREAST_VAR_ID [ ch_P ]) 1) (PREAST_EXPR_ID (PREAST_VAR_ARRAY (PREAST_VAR_ID [ ch_Q ]) (PREAST_EXPR_BYTE8 〈x0,x1〉)))
- ]
- )
- )
- ]
- )
-).
-
-lemma checkprova : None ? = preast_to_ast prova.
-normalize;
-*)