type-of-s := λ(: compound AST). (: ( (let r TAny) (match compound ( () ( (Lit( tt _ )) ( (let nt (parse-type tt)) (set r nt) )) ( (Var( tt _ )) ( (let nt (parse-type tt)) (set r nt) )) ( (App( (App( lt (Lit( ',_s _ )) )) rt )) ( (let ltt (type-of-s lt)) (let rtt (type-of-s rt)) (set r (t3( 'Cons_s ltt rtt ))) )) ( _ (exit-error( 'Malformed\sType\sDefinition_s compound ))) )) r ) Type);