Commit ebe29a7b authored by POTTIER Francois's avatar POTTIER Francois

First run of the typechecker.

parent 6ad4282d
module T = FTypeChecker
open Printf
open AlphaLib
open F
open FTypeChecker
let identity : raw_term =
TeTyAbs ("A", TeAbs ("x", TyArrow (TyVar "A", TyVar "A"), TeVar "x"))
let identity : nominal_term =
import_term KitImport.empty identity
let ty : nominal_typ =
typeof identity
let ty : raw_typ =
export_typ KitExport.empty ty
let () =
printf "Success.\n%!"
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment