Library Extract





Require
 Import
 Termes
.

Require
 Import
 Conv
.

Require
 Import
 Types
.

Require
 Import
 Conv_Dec
.

Require
 Import
 Infer
.




  Extract
 Inductive
 bool
 => "bool" [ "true" "false" ].

  Extract
 Inductive
 sumbool
 => "bool" [ "true" "false" ].

  Extract
 Inductive
 sumor
 => "option" [ "Some" "None" ].




 Extraction
 "infer" eqterm
 red_to_sort
 red_to_prod
 infer
 check_typ
 add_typ
.