diff --git a/Yices/Painless/Language.hs b/Yices/Painless/Language.hs
--- a/Yices/Painless/Language.hs
+++ b/Yices/Painless/Language.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE ScopedTypeVariables    #-}
 {-# LANGUAGE PatternGuards          #-}
 {-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FlexibleContexts       #-}
 {-# LANGUAGE OverlappingInstances   #-}
 {-# LANGUAGE UndecidableInstances   #-}
 {-# LANGUAGE MultiParamTypeClasses  #-}
@@ -52,6 +53,26 @@
 -- > x1 => 0b100
 -- > Satisfiable
 --
+-- /Uninterpreted functions/
+--
+-- > {-# LANGUAGE ScopedTypeVariables #-}
+-- > import Yices.Painless.Language
+-- >
+-- > main = print =<< solve p
+-- >
+-- > p f g (n :: Exp Int) = f n &&* g (f n)
+--
+-- Returns an assignment to the variables, and a model for the functions
+-- (using Yices pretty printer):
+--
+-- > $ runhaskell ex0.hs
+-- > x0 => 1
+-- >
+-- > (= x0 1)
+-- > (= (f2 1) true)
+-- > (= (f1 true) true)
+--
+-- > Satisfiable
 
 module Yices.Painless.Language (
 
@@ -60,6 +81,7 @@
 
     -- * Building Yices propositions.
     Yices, Exp,
+    BitVector,
 
     -- ** Scalar introduction
     -- constant,
@@ -71,6 +93,9 @@
     -- ** Bit vectors
     -- $BitInstances
 
+    -- ** Uninterpreted functions
+    -- $Functions
+
     -- ** Conditional expressions
     (?),
 
@@ -86,12 +111,15 @@
     -- * Design discussion
     -- $Notes
 
+    module Data.Bits
+
   ) where
 
 import Prelude hiding (not, or, and, min, max)
 
 import Data.Typeable
 import qualified Data.Map as M
+import Data.Maybe
 
 import Data.Bits
 
@@ -134,6 +162,16 @@
 -- into their symbolic form.
 --
 
+-- $Functions
+-- 
+-- Uninterpreted functions may be introduced as variables (alongside
+-- scalar variables). 
+--
+-- E.g.
+--
+-- > \f g x -> f (g x) ==* 7
+--
+
 ------------------------------------------------------------------------
 -- Language
 
@@ -469,9 +507,13 @@
 data Exp t where
 
     -- Needed for conversion to de Bruijn form
-    Tag         :: (IsScalar t) => Int          ->  Exp t
-                 -- environment size at defining occurrence
+    Tag         :: (IsAType t) => Int          ->  Exp t
 
+    -- NNN
+    TagFn       :: (IsAType (a -> b)) => Int   ->  (Exp a -> Exp b)
+                 -- application of a symbolic function to an argument.
+                 -- TODO: basically, a restricted form of application.  Sort this out.
+
     Const       :: (Show t, IsScalar t)
                 => t                             -> Exp t
 
@@ -531,13 +573,24 @@
   -- Convert expressions
   convert lyt e = OBody (convertOpenExp lyt e)
 
-instance (IsScalar a, Yices f r) => Yices (Exp a -> f) (a -> r) where
+instance (IsAType a, IsScalar a, Yices f r) => Yices (Exp a -> f) (a -> r) where
   -- Convert binders, one bind at a time.
   convert lyt f = OLam (convert lyt' (f a))
     where
     a    = Tag (size lyt)
     lyt' = inc lyt `PushLayout` ZeroIdx
 
+
+--    No instance for (Yices ((Exp Int -> Exp Int) -> Exp Int -> Exp Bool) r)
+
+-- Convert functions. Identical for the other recursive case.
+instance (IsScalar a, IsScalar b, Yices f r)
+                => Yices ((Exp a -> Exp b) -> f) ((a -> b) -> r) where
+  convert lyt f = OLam (convert lyt' (f g))
+    where
+    g    = TagFn (size lyt) -- :: Exp a -> Exp b -- generate a fresh, anonymous function!
+    lyt' = inc lyt `PushLayout` ZeroIdx
+
 ------------------------------------------------------------------------
 
 -- |Conversion from HOAS to de Bruijn expression AST
@@ -565,6 +618,8 @@
   where
     cvt :: Exp t' -> OpenExp env t'
     cvt (Tag i)             = Var (prjIdx (size lyt - i - 1) lyt) -- indexing!
+    cvt (TagFn i arg)       = VarFn (prjIdx (size lyt - i - 1) lyt) (cvt arg)-- indexing!
+            --  application.
     cvt (Const v)           = OConst v
     cvt (Tuple tup)         = OTuple (convertTuple lyt tup)
     cvt (Cond e1 e2 e3)     = OCond (cvt e1) (cvt e2) (cvt e3)
@@ -670,8 +725,9 @@
 -- |Function abstraction
 --
 data OpenFun env t where
-  OBody ::               OpenExp env      t -> OpenFun env t
-  OLam  :: IsScalar a => OpenFun (env, a) t -> OpenFun env (a -> t)
+  OBody ::                   OpenExp env      t -> OpenFun env t
+  -- OLam  :: {-IsScalar a =>-} OpenFun (env, a) t -> OpenFun env (a -> t)
+  OLam  :: IsAType a => OpenFun (env, a) t -> OpenFun env (a -> t)
 
 -- |Function without free scalar variables
 --
@@ -686,11 +742,15 @@
 --
 data OpenExp env t where
 
-  -- Variable index, ranging only over tuples or scalars
-  Var         :: IsScalar t
+  -- Variable index
+  Var         :: IsAType t
               => Idx env t
               -> OpenExp env t
 
+  VarFn       :: IsAType (a -> b) =>
+                 Idx env (a -> b) -> (OpenExp env a -> OpenExp env b)
+                 -- TODO: restricted form of application
+
   -- Constant values
   OConst      :: (Show t, IsScalar t)
               => t
@@ -837,18 +897,25 @@
 
 prettyFun ::  Int -> OpenFun env a -> Doc
 prettyFun lvl fun =
-  let (n, bodyDoc) = count fun
+  let (n, vs, bodyDoc) = count fun
   in
     if n < 0 
         then bodyDoc
         else 
-          char '\\' <> hsep [text $ "x" ++ show idx | idx <- reverse [0..n]] <+>
+          char '\\' <> hsep [text $ case ei of Left i -> "f"  ++ show i ;
+                                               Right i -> "x" ++ show i
+                            | ei <- vs] <+>
           text "->" <+> bodyDoc
   where
-     count :: OpenFun env fun -> (Int, Doc)
-     count (OBody body) = (-1, prettyExp lvl noParens body)
-     count (OLam fun')  = let (n, body) = count fun' in (1 + n, body)
+     count :: OpenFun env fun -> (Int, [Either Int Int], Doc)
+     count (OBody body) = ((-1), [], prettyExp lvl noParens body)
 
+     count (OLam (f :: OpenFun (env, a) t))  | (AFunctionType _ _)  <- aType :: AType a =
+              let (n, vs, body) = count f in (1 + n, Left (1+n) : vs, body)
+
+     count (OLam (f :: OpenFun (env, a) t))  =
+              let (n, vs, body) = count f in (1 + n, Right (1+n) : vs, body)
+
 -- Pretty print an expression.
 --
 -- * Apply the wrapping combinator (1st argument) to any compound expressions.
@@ -856,7 +923,9 @@
 prettyExp :: forall t env .
              Int -> (Doc -> Doc) -> OpenExp env t -> Doc
 
+-- TODO: function types
 prettyExp _   _    (Var idx)         = text $ "x" ++ show (idxToInt idx)
+prettyExp lvl wrap (VarFn idx e)     = text ( "f" ++ show (idxToInt idx)) <+> prettyExp lvl wrap e
 prettyExp _   _    (OConst v)        = text $ show (v :: t) -- dispatch differently for BitVector types
 prettyExp lvl _    (OTuple tup)      = prettyTuple lvl tup
 
@@ -934,7 +1003,7 @@
     Yices.setTypeChecker True
 
     let t = convertYices q -- bind all the variables
-    print t
+    -- print t
 
     (g,e) <- execY c t 
 
@@ -953,7 +1022,7 @@
                 Nothing -> return Yices.Satisfiable
                 Just m  -> do
 
-                    vs <- sequence
+                    vs <- catMaybes `fmap` sequence
                             [ get m v t' d
                             | (v,(t',d)) <- M.toList g ]
 
@@ -963,25 +1032,32 @@
                                     Nothing -> putStrLn "_"
                                     Just v  -> print v)
 
+                    -- TODO: extract functions.
+                    Yices.display m
+
                     -- print cs
                     return Yices.Satisfiable
 
--- | Retrieving bindings by type
+-- | Retrieving bindings by type (can't retrieve functions)
 --
-get :: Yices.Model -> String -> YType -> Yices.Decl -> IO (String, YValue)
-get m v (YType (ty :: ScalarType t)) d
+get :: Yices.Model -> String -> YType -> Yices.Decl -> IO (Maybe (String, YValue))
+get m v (YType (ty :: AType t)) d
 
-    | NumScalarType (IntegralNumType (TypeInt _))  <- ty
+    | AScalarType (NumScalarType (IntegralNumType (TypeInt _)))  <- ty
     = do mn <- Yices.getValueInt m d
-         return (v, YValue mn)
+         return $ Just (v, YValue mn)
 
-    | NonNumScalarType (TypeBool _)                <- ty
+    | AScalarType (NonNumScalarType (TypeBool _))               <- ty
     = do mn <- Yices.getValueBool m d
-         return (v, YValue mn)
+         return $ Just (v, YValue mn)
 
-    | NumScalarType (IntegralNumType (TypeVectorBool _))               <- ty
+    | AScalarType (NumScalarType (IntegralNumType (TypeVectorBool _)))              <- ty
     = do mn <- Yices.getValueBitVector m d (fromIntegral $ 8 * sizeOf (undefined :: Word))
-         return (v, YValue $ fmap BitVector mn)
+         return $ Just (v, YValue $ fmap BitVector mn)
+
+    -- Can't return function models?
+    | AFunctionType _ _ <- ty
+    = return Nothing
             
     | otherwise = error "Yices.Painless.get: don't know how to get this type yet"
 
@@ -992,9 +1068,9 @@
 --
 type YEnv = M.Map String (YType, Yices.Decl)
 
-data YType  = forall a. IsScalar a => YType (ScalarType a)
+data YType  = forall a. IsAType a => YType (AType a)
 
-data YValue = forall a. (Show a, IsScalar a) => YValue (Maybe a)
+data YValue = forall a. (Show a, IsAType a) => YValue (Maybe a)
 
 --
 -- To run,
@@ -1013,42 +1089,70 @@
 -- Declaring variables. Begin with a closed Yices program.
 --
 execF :: Yices.Context -> OFun t -> IO (YEnv, Yices.Expr)
-execF c fn = go fn 0 M.empty
+execF c fn = go fn (count fn) M.empty
     where
+        -- determine size of environment
+        count :: OpenFun env f -> Int
+        count (OBody _) = (-1)
+        count (OLam f)  = 1 + count f
+
         go :: OpenFun env u -> Int -> YEnv -> IO (YEnv, Yices.Expr)
         go (OBody b) _ g = (,) g <$> exec c b
 
         -- Numbers
         go (OLam (f :: OpenFun (env, a) t)) n g
-            | ty@(NumScalarType (IntegralNumType (TypeInt _)))  <- scalarType :: ScalarType a
+            | ty@(AScalarType (NumScalarType (IntegralNumType (TypeInt _))))  <- aType :: AType a
             = do
                 let nm = "x" ++ show n -- we get to actually name things
                 tynm <- Yices.mkType c "int"
                 d    <- Yices.mkVarDecl c nm tynm
-                go f (n + 1) (M.insert nm (YType ty, d) g)
+                go f (n - 1) (M.insert nm (YType ty, d) g)
         
         -- Booleans
         go (OLam (f :: OpenFun (env, a) t)) n g
-            | ty@(NonNumScalarType (TypeBool _))                <- scalarType :: ScalarType a
+            | ty@(AScalarType (NonNumScalarType (TypeBool _)))              <- aType :: AType a
             = do
                 let nm = "x" ++ show n
                 d <- Yices.mkBoolDecl c nm
-                go f (n + 1) (M.insert nm (YType ty, d) g)
+                go f (n - 1) (M.insert nm (YType ty, d) g)
 
         -- Bit vectors
         go (OLam (f :: OpenFun (env, a) t)) n g
-            | ty@(NumScalarType (IntegralNumType (TypeVectorBool _)))   <- scalarType :: ScalarType a
+            | ty@(AScalarType (NumScalarType (IntegralNumType (TypeVectorBool _))))  <- aType :: AType a
             = do
                 let nm = "x" ++ show n
                 -- TODO: hack, no size information for bit vectors yet.
                 -- TODO: show bvs in a better form.
                 tynm <- Yices.mkBitVectorType c (fromIntegral $ 8 * sizeOf (undefined :: Word))
                 d    <- Yices.mkVarDecl c nm tynm
-                go f (n + 1) (M.insert nm (YType ty, d) g)
+                go f (n - 1) (M.insert nm (YType ty, d) g)
 
+        -- Uninterpreted functions
+        go (OLam (f :: OpenFun (env, a) t)) n g
+            | ty@(AFunctionType
+                        [a] 
+                        r 
+                        )  <- aType :: AType a
+           = do let nm = "f" ++ show n -- we get to actually name things
+                argty <- toBuiltInYicesType c a
+                resty <- toBuiltInYicesType c r
+                tynm <- Yices.mkFunctionType c [argty] resty
+                d    <- Yices.mkVarDecl c nm tynm
+                go f (n - 1) (M.insert nm (YType ty, d) g)
 
         go _ _ _ = error "Yices.execF: don't know how to bind variables of this type yet"
 
+
+-- Only built in types.
+-- number, real, int, nat, bool, any
+toBuiltInYicesType :: Yices.Context -> ScalarType a -> IO Yices.Type
+toBuiltInYicesType c a = case a of
+        (NumScalarType (IntegralNumType (TypeInt _))) -> Yices.mkType c "int"
+        (NonNumScalarType (TypeBool _))               -> Yices.mkType c "bool"
+        _ -> error $ "Don't know how to bind this type yet: " ++ show a
+
+-- TODO: map ScalarTypes to yices strings.
+
 -- | Execute an expression with free variables.
 --
 -- /TODO:/
@@ -1084,6 +1188,22 @@
     case v of
         Nothing -> error "Undefined variable"
         Just d  -> Yices.mkVarFromDecl c d
+
+-- Application
+exec c (VarFn i e) = do
+    let n = "f" ++ show (idxToInt i)
+    v  <- Yices.getVarDeclFromName c n -- sneaky. using Yices environment. TODO: use YEnv
+--    print n
+
+    -- get our yices function
+    yf <- case v of
+        Nothing -> error $ "Undefined variable: " ++ show n
+        Just d  -> Yices.mkVarFromDecl c d
+
+    -- compile the expression
+    ye <- exec c e
+
+    Yices.mkApp c yf [ye]
 
 -- Conditionals
 exec c (OCond b t e) = do
diff --git a/Yices/Painless/Type.hs b/Yices/Painless/Type.hs
--- a/Yices/Painless/Type.hs
+++ b/Yices/Painless/Type.hs
@@ -214,6 +214,12 @@
   NumScalarType    :: NumType a    -> ScalarType a
   NonNumScalarType :: NonNumType a -> ScalarType a
 
+-- | All Yices types: functions over scalar types, or scalar types.
+data AType a where
+  AFunctionType     :: [ScalarType t] -> ScalarType r -> AType  (t -> r)
+    --  todo: tuples
+  AScalarType       :: ScalarType a -> AType a
+
 -- Showing type names
 -- 
 
@@ -266,6 +272,7 @@
 -- Querying scalar type representations
 -- 
 
+
 -- |Integral types
 --
 class (IsScalar a, IsNum a, IsBounded a) => IsIntegral a where
@@ -515,6 +522,17 @@
 
 instance IsBounded CUChar where
   boundedType = NonNumBoundedType nonNumType
+
+-- | All types we can bind
+class Typeable a => IsAType a where
+  aType    :: AType a
+
+instance IsAType Int where
+  aType    = AScalarType scalarType
+
+instance (IsScalar a, IsScalar b) => IsAType (a -> b) where
+  aType    = AFunctionType [scalarType] scalarType
+    -- todo: tuples
 
 -- |All scalar type
 --
diff --git a/tests/examples/ex24.hs b/tests/examples/ex24.hs
deleted file mode 100644
--- a/tests/examples/ex24.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-import Yices.Painless.Language
-
-main = print =<< solve p
-
-data S = S1 | S2 | S3
-    deriving (Show, Enum)
-
-p x1 x2 x3 x4 = 
-    and 
-      [ (/=*) x1 x2
-      , (/=*) x1 x3
-      , (/=*) x1 x4
-      , (/=*) x2 x3
-      , (/=*) x2 x4
-      , (/=*) x3 x4
-      ]
diff --git a/tests/examples/ex5.ys b/tests/examples/ex5.ys
deleted file mode 100644
--- a/tests/examples/ex5.ys
+++ /dev/null
@@ -1,18 +0,0 @@
-
-(define-type pc (scalar sleeping trying critical))
-(define f::(-> pc pc))
-(define g::(-> pc pc))
-(define x1::pc)
-(define x2::pc)
-(define x3::pc)
-(define x4::pc)
-(define x5::pc)
-(define x6::pc)
-
-
-
-(assert (/= (g (f x1)) (g (f x2))))
-(assert (= x1 x3))
-(assert (= x1 x4))
-(assert (= x3 x2))
-
diff --git a/tests/examples/ex6.ys b/tests/examples/ex6.ys
deleted file mode 100644
--- a/tests/examples/ex6.ys
+++ /dev/null
@@ -1,18 +0,0 @@
-
-(define-type pc (scalar sleeping trying critical))
-(define f::(-> pc pc))
-(define g::(-> pc pc))
-(define x1::pc)
-(define x2::pc)
-(define x3::pc)
-(define x4::pc)
-(define x5::pc)
-(define x6::pc)
-
-
-
-(assert (= x1 x3))
-(assert (= x1 x4))
-(assert (= x3 x2))
-(assert (/= (g (f x1)) (g (f x2))))
-
diff --git a/yices-painless.cabal b/yices-painless.cabal
--- a/yices-painless.cabal
+++ b/yices-painless.cabal
@@ -1,5 +1,5 @@
 Name:                yices-painless
-Version:             0.1.1
+Version:             0.1.2
 Synopsis:            An embedded language for programming the Yices SMT solver
 Description:         
     This library defines an embedded language in Haskell for programming
@@ -13,14 +13,16 @@
     MaxSMT (and, dually, unsat cores) and is competitive as an ordinary
     SAT and MaxSAT solver.
     .
-    The embedded language embeds both terms and types into Haskell, via
-    a typed higher-order abstract syntax representation. Propositions in
-    the embedding are represented as (typed) pure expressions.
+    The embedded language embeds both terms, functions and types into
+    Haskell, via a typed higher-order abstract syntax representation.
+    Propositions in the embedding are represented as (typed) pure
+    expressions.
     .
     Solution variables in the proposition (notionally, free variables)
     are bound an the outermost lambda term. Propositions constructed
     from logical primitives can then be executed by the solver to yield
     a satisfying assignment to those free variables in the proposition.
+    Uninterpreted functions may be introduced via variables as well.
     .
     More information about Yices:
     .