Module DemoExtract
Require
Import
DemoHeader
DemoTarget
.
Extract
Inductive
list
=> "
list
" [ "[]" "(::)" ].
Extract
Inlined
Constant
Datatypes.fst
=> "
fst
".
Extract
Inlined
Constant
Datatypes.snd
=> "
snd
".
Extract
Inductive
prod
=> "