diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-12-26 12:50:42 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-12-26 12:50:42 -0500 |
| commit | 4434fc4ce2f819f3965e39b5aff6be65cdc8d392 (patch) | |
| tree | f3ddc329802096a5492e96b26e2ee3f81ddd273d /src | |
| parent | a3c02c642d9146bfe281a7f7727a5fa761305e0f (diff) | |
Add flatten_flat_type
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Syntax.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 2a6cce891..f9be9f318 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -421,6 +421,12 @@ Global Arguments Tbase {_}%type_scope _%ctype_scope. Ltac admit_Wf := apply Wf_admitted. +Fixpoint flatten_flat_type {base_type_code} (t : flat_type (flat_type base_type_code)) : flat_type base_type_code + := match t with + | Tbase T => T + | Prod A B => Prod (@flatten_flat_type _ A) (@flatten_flat_type _ B) + end. + Scheme Equality for flat_type. Scheme Equality for type. |