-nlet rec ast_type_rect_aux (P:ast_type → Type)
- (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
- (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
- (f2:Πt.P t)
- (t:ne_list ast_type) on t ≝
- match t return λt.P (AST_TYPE_STRUCT t) with
- [ ne_nil h ⇒ f h (f2 h)
- | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rect_aux P f f1 f2 t)
- ].
-
-nlet rec ast_type_rect (P:ast_type → Type)
- (f:Πb.P (AST_TYPE_BASE b))
- (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
- (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
- (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
- (t:ast_type) on t : P t ≝
- match t return λt.P t with
- [ AST_TYPE_BASE b ⇒ f b
- | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rect P f f1 f2 f3 t')
- | AST_TYPE_STRUCT nl ⇒ match nl with
- [ ne_nil h ⇒ f2 h (ast_type_rect P f f1 f2 f3 h)
- | ne_cons h t ⇒ f3 h t (ast_type_rect P f f1 f2 f3 h) (ast_type_rect_aux P f2 f3 (ast_type_rect P f f1 f2 f3) t)
- ]
- ].
-*)