Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940
(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)
(*type denv = { ty_subst : Expr.Ty.subst;}
type dacc = { unit : unit;}
type uenv = { unit : unit;}
type uacc = { unit : unit;}
let rec normalize_ty k denv dacc ty = match Expr.Ty.descr ty with | Expr.TyVar v -> normalize_ty_var k denv dacc v | Expr.TyApp (f, args) -> normalize_ty_app k denv dacc f args | Expr.Arrow (params, ret) -> normalize_ty_arrow k denv dacc params ret | Expr.Pi (vars, body) -> normalize_ty_pi k denv dacc vars body
and normalize_ty_var k denv dacc v = assert false
and normalize_ty_app k denv dacc f args = assert false
and normalize_ty_arrow k denv dacc params ret = assert false
and normalize_ty_pi k denv dacc vars body = assert false*)