diff options
Diffstat (limited to 'contrib/extraction/test_extraction.v')
| -rw-r--r-- | contrib/extraction/test_extraction.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v index 57ce3cf868..451ffafeff 100644 --- a/contrib/extraction/test_extraction.v +++ b/contrib/extraction/test_extraction.v @@ -89,3 +89,7 @@ Extraction tree_size. Extraction Cases (left True True I) of (left x)=>(S O) | (right x)=>O end. Extraction sumbool_rec. + +Definition horibilis := [b:bool]<[b:bool]if b then Type else nat>if b then Set else O. + +Extraction horibilis.
\ No newline at end of file |