typelevel-rewrite-rules-0.1: Solve type equalities using custom type-level rewrite rules

Safe HaskellSafe
LanguageHaskell2010

TypeLevel.Rewrite.Internal.Term

Synopsis

Documentation

atomTerm :: f -> Term f v Source #

an expression like (as ++ '[]) ++ bs would be represented as Fun appendTyCon [Var "as", Fun nilTyCon [] or rather Fun appendTyCon [Fun starTyCon [], Var "as", Fun nilTyCon [Fun starTyCon []] because those polymorphic TyCons need to be specialized to the * kind