diff --git a/Ivor/Datatype.lhs b/Ivor/Datatype.lhs
--- a/Ivor/Datatype.lhs
+++ b/Ivor/Datatype.lhs
@@ -6,6 +6,7 @@
 > import Ivor.Nobby
 > import Ivor.PatternDefs
 > import Ivor.Errors
+> import Ivor.Values
 
 > import Debug.Trace
 
@@ -42,8 +43,8 @@
 >	        }
 >       deriving Show
 
-> getPat (Sch p i) = p
-> getRed (Sch p i) = i
+> getPat (Sch p _ i) = p
+> getRed (Sch p _ i) = i
 
 > getArity [] = 2 -- empty data type should have elim rule of arity 2!
 >                 -- (actually not if they're dependent. Fix this.)
@@ -102,7 +103,7 @@
 >     do let ps = map (mkPat gamma) pats
 >	 let rhsvars = getPatVars gamma ps
 >        let rhs = substVars gamma n rhsvars ret
->	 return (Sch (reverse ps) (Ind rhs))
+>	 return (Sch (reverse ps) [] (Ind rhs))
 
 Make a pattern from a raw term. Anything weird, just make it a "PTerm".
 
diff --git a/Ivor/Display.lhs b/Ivor/Display.lhs
--- a/Ivor/Display.lhs
+++ b/Ivor/Display.lhs
@@ -8,6 +8,7 @@
 > import Ivor.TTCore
 > import Ivor.Typecheck
 > import Ivor.Nobby
+> import Ivor.Values
 
 > displayHoleContext :: Gamma Name -> [Name] -> Name -> Indexed Name -> String
 > displayHoleContext gam hidden h tm = 
diff --git a/Ivor/Errors.lhs b/Ivor/Errors.lhs
--- a/Ivor/Errors.lhs
+++ b/Ivor/Errors.lhs
@@ -10,6 +10,7 @@
 >             | IMessage String
 >             | IUnbound (Indexed Name) (Indexed Name) (Indexed Name) (Indexed Name) [Name]
 >             | INoSuchVar Name
+>             | ICantInfer Name (Indexed Name)
 >             | IContext String IError
 >   deriving (Show, Eq)
 
@@ -20,3 +21,12 @@
 > type IvorM = Either IError
 
 > ifail = Left
+
+Generic error checking can go here:
+
+Check that all the names are real rather than implicit and inferred
+
+> checkRealNames :: [Name] -> Indexed Name -> IvorM ()
+> checkRealNames [] tm = return ()
+> checkRealNames (nm@(MN ("INFER", n)): ns) tm = ifail (ICantInfer nm tm)
+> checkRealNames (_:ns) tm = checkRealNames ns tm
diff --git a/Ivor/Evaluator.lhs b/Ivor/Evaluator.lhs
--- a/Ivor/Evaluator.lhs
+++ b/Ivor/Evaluator.lhs
@@ -1,28 +1,42 @@
 > {-# OPTIONS_GHC -fglasgow-exts #-}
 
-> module Ivor.Evaluator(eval_whnf, eval_nf) where
+> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_without, eval_nf_limit,
+>                       eval_nfEnv, tidyNames) where
 
 > import Ivor.TTCore
 > import Ivor.Gadgets
 > import Ivor.Constant
-> import Ivor.Nobby
-> import Ivor.Typecheck
+> import Ivor.Values
 
 > import Debug.Trace
 > import Data.Typeable
+> import Control.Monad.State
+> import List
+> import qualified Data.Map as Map
 
  data Machine = Machine { term :: (TT Name),
                           mstack :: [TT Name],
                           menv :: [(Name, Binder (TT Name))] }
 
 > eval_whnf :: Gamma Name -> Indexed Name -> Indexed Name
-> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm)
+> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm Nothing Nothing)
 >                              in finalise (Ind res)
 
 > eval_nf :: Gamma Name -> Indexed Name -> Indexed Name
-> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm)
+> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing)
 >                            in finalise (Ind res)
 
+> eval_nf_without :: Gamma Name -> Indexed Name -> [Name] -> Indexed Name
+> eval_nf_without gam tm [] = eval_nf gam tm
+> eval_nf_without gam (Ind tm) ns = let res = makePs (evaluate True gam tm (Just ns) Nothing)
+>                                       in finalise (Ind res)
+
+> eval_nf_limit :: Gamma Name -> Indexed Name -> [(Name, Int)] -> Indexed Name
+> eval_nf_limit gam tm [] = eval_nf gam tm
+> eval_nf_limit gam (Ind tm) ns 
+>     = let res = makePs (evaluate True gam tm Nothing (Just ns))
+>           in finalise (Ind res)
+
 > type Stack = [TT Name]
 > type SEnv = [(Name, TT Name, TT Name)]
 
@@ -40,82 +54,137 @@
 [[let x = t in e]]	xs	es	[[e]], xs, (Let x t: es)
 
 > evaluate :: Bool -> -- under binders? 'False' gives WHNF
->             Gamma Name -> TT Name -> TT Name
-> evaluate open gam tm = eval tm [] [] []
+>             Gamma Name -> TT Name -> 
+>             Maybe [Name] ->  -- Names not to reduce
+>             Maybe [(Name, Int)] -> -- Names to reduce a maximum number
+>             TT Name
+> evaluate open gam tm jns maxns = -- trace ("EVALUATING: " ++ debugTT tm) $ 
+>                                  let res = evalState (eval tm [] [] []) maxns
+>                                      in {- trace ("RESULT: " ++ debugTT res) -} 
+>                                         res
 >   where
->     eval :: TT Name -> Stack -> SEnv -> [(Name, TT Name)] -> TT Name
->     eval (P x) xs env pats 
->         = case lookup x pats of
->              Nothing -> evalP x (lookupval x gam) xs env pats
->              Just val -> eval val xs env pats
->     eval (V i) xs env pats = if (length env>i) 
->                                then eval (getEnv i env) xs env pats
->                                else unload (V i) xs pats env -- blocked, so unload
->     eval (App f a) xs env pats = eval f ((eval a [] env pats):xs) env pats
->     eval (Bind n (B Lambda ty) (Sc sc)) xs env pats =
->         let ty' = eval ty [] env pats in
->             evalScope n ty' sc xs env pats
->     eval (Bind n (B Pi ty) (Sc sc)) xs env pats =
->         let ty' = eval ty [] env pats in
->            unload (Bind n (B Pi ty') (Sc sc)) [] pats env
->     eval (Bind n (B (Let val) ty) (Sc sc)) xs env pats =
->         eval sc xs ((n,ty,eval val [] env pats):env) pats
->     eval (Bind n (B bt ty) (Sc sc)) xs env pats =
->         let ty' = eval ty [] env pats in
->            unload (Bind n (B bt ty') (Sc sc)) [] pats env
->     eval x stk env pats = unload x stk pats env
+>     eval :: TT Name -> Stack -> SEnv -> 
+>             [(Name, TT Name)] -> State (Maybe [(Name, Int)]) (TT Name)
+>     eval tm stk env pats = {- trace (show (tm, stk, env, pats)) $ -} eval' tm stk env pats
 
+>     eval' (P x) xs env pats 
+>         = do mns <- get
+>              let (use, mns') = usename x jns mns
+>              put mns'
+>              case lookup x pats of
+>                 Nothing -> if use then evalP x (lookupval x gam) xs env pats
+>                                   else evalP x Nothing xs env pats
+>                 Just val -> eval val xs env (removep x pats)
+>        where removep n [] = []
+>              removep n ((x,t):xs) | n==x = removep n xs
+>                                   | otherwise = (x,t):(removep n xs)
+>     eval' (V i) xs env pats 
+>              = if (length env>i) 
+>                   then eval (getEnv i env) xs env pats
+>                   else unload (V i) xs pats env -- blocked, so unload
+>     eval' (App f a) xs env pats 
+>        = do a' <- eval a [] env pats
+>             eval f (a':xs) env pats
+>     eval' (Bind n (B Lambda ty) (Sc sc)) xs env pats
+>        = do ty' <- eval ty [] env pats
+>             evalScope Lambda n ty' sc xs env pats
+>     eval' (Bind n (B Pi ty) (Sc sc)) xs env pats
+>        = do ty' <- eval ty [] env pats
+>             evalScope Pi n ty' sc xs env pats
+>            -- unload (Bind n (B Pi ty') (Sc sc)) [] pats env
+>     eval' (Bind n (B (Let val) ty) (Sc sc)) xs env pats 
+>        = do val' <- eval val [] env pats
+>             eval sc xs ((n,ty,val'):env) pats
+>     eval' (Bind n (B bt ty) (Sc sc)) xs env pats
+>        = do ty' <- eval ty [] env pats
+>             unload (Bind n (B bt ty') (Sc sc)) [] pats env
+>     eval' x stk env pats = unload x stk pats env
+
 >     evalP n (Just v) xs env pats 
 >        = case v of
 >             Fun opts (Ind v) -> eval v xs env pats
->             PatternDef p _ -> pmatch n p xs env pats
+>             PatternDef p _ _ -> pmatch n p xs env pats
 >             PrimOp _ f -> case f xs of
 >                             Nothing -> unload (P n) xs pats env
 >                             Just v -> eval v [] env pats
 >             _ -> unload (P n) xs pats env
 >     evalP n Nothing xs env pats = unload (P n) xs pats env -- blocked, so unload stack
 
->     evalScope n ty sc (x:xs) env pats = eval sc xs ((n,ty,x):env) pats
->     evalScope n ty sc [] env pats
->       | open = let n' = uniqify n (map sfst env)
->                    newsc = pToV n' (eval sc [] ((n',ty,P n'):env) pats) in
->                    buildenv env $ unload (Bind n' (B Lambda ty) newsc)
->                                          [] pats env
+>     evalScope b n ty sc (x:xs) env pats = eval sc xs ((n,ty,x):env) pats
+>     evalScope b n ty sc [] env pats
+>       | open = do let n' = uniqify' n (map sfst env ++ map fst pats)
+>                   let  tmpname = (MN ("E", length env))
+>                   sc' <- eval sc [] ((n',ty,P tmpname):env) pats
+>                   let newsc = pToV tmpname sc'
+>                   u' <- unload (Bind n' (B b ty) newsc) [] pats env
+>                   return $ buildenv env u'
 >       | otherwise 
->          = buildenv env $ unload (Bind n (B Lambda ty) (Sc sc)) [] pats env -- in Whnf
+>          = do let n' = uniqify' n (map sfst env ++ map fst pats)
+>               u' <-  unload (Bind n' (B Lambda ty) (Sc sc)) [] pats env -- in Whnf
+>               return $ buildenv env u'
 >     unload x [] pats env 
->                = foldl (\tm (n,val) -> substName n val (Sc tm)) x pats
+>                = return $ foldl (\tm (n,val) -> substName n val (Sc tm)) x pats
 >     unload x (a:as) pats env = unload (App x a) as pats env
+>
+>     uniqify' u@(UN n) ns = uniqify (MN (n,0)) ns
+>     uniqify' n ns = uniqify n ns
 
+>     usename x Nothing Nothing = (True, Nothing)
+>     usename x _ (Just ys) = case lookup x ys of
+>                               Just 0 -> (False, Just ys)
+>                               Just n -> (True, Just (update x (n-1) ys))
+>                               _ -> (True, Just ys)
+>     usename x (Just xs) m = (not (elem x xs), m)
+
+>     update x v [] = []
+>     update x v ((k,_):xs) | x == k = ((x,v):xs)
+>     update x v (kv:xs) = kv : update x v xs
+
 >     buildenv [] t = t
 >     buildenv ((n,ty,tm):xs) t 
 >                 = buildenv xs (subst tm (Sc t))
 >     --            = buildenv xs (Bind n (B (Let tm) ty) (Sc t))
 
+>     renameRHS pbinds rhs env = rrhs [] [] (nub pbinds) rhs where
+>       rrhs namemap pbinds' [] rhs = {-trace ("BEFORE " ++ show (rhs, pbinds, pbinds')) $ -}
+>                                     (pbinds', substNames namemap rhs)
+>       rrhs namemap pbinds ((n,t):ns) rhs
+>          = let n' = uniqify' (UN (show n)) (map sfst env ++ map fst pbinds ++ map fst ns) in
+>                rrhs ((n,P n'):namemap) ((n',t):pbinds) ns rhs
+
+>     substNames [] rhs = {-trace ("AFTER " ++ show rhs) $ -} rhs
+>     substNames ((n,t):ns) rhs = substNames ns (substName n t (Sc rhs))
+
 >     pmatch n (PMFun i clauses) xs env pats = 
->         case matches clauses xs env pats of
->           Nothing -> unload (P n) xs pats env
->           Just (rhs, pbinds, stk) -> eval rhs stk env pbinds
+>         do cm <- matches clauses xs env pats
+>            case cm of
+>              Nothing -> unload (P n) xs pats env
+>              Just (rhs, pbinds, stk) -> 
+>                    let (pbinds', rhs') = renameRHS pbinds rhs env in
+>                        eval rhs' stk env pbinds'
 
->     matches [] xs env pats = Nothing
+>     matches [] xs env pats = return Nothing
 >     matches (c:cs) xs env pats 
->        = case (match c xs env pats) of
->            Just v -> Just v
->            Nothing -> matches cs xs env pats
+>        = do cm <- (match c xs env pats)
+>             case cm of
+>               Just v -> return $ Just v
+>               Nothing -> matches cs xs env pats
 
->     match :: Scheme Name -> [TT Name] -> SEnv -> [(Name, TT Name)] ->
->              Maybe (TT Name, [(Name, TT Name)], Stack)
->     match (Sch pats rhs) xs env patvars 
->               = matchargs pats xs rhs env patvars
->     matchargs [] xs (Ind rhs) env patvars = Just (rhs, patvars, xs)
->     matchargs (p:ps) (x:xs) rhs env patvars
->               = case matchPat p (eval x [] env patvars) patvars of
->                   Just patvars' -> matchargs ps xs rhs env patvars'
->                   Nothing -> Nothing
->     matchargs _ _ _ _ _ = Nothing
+>     match :: Scheme Name -> [TT Name] -> SEnv -> 
+>              [(Name, TT Name)] ->
+>              State (Maybe [(Name, Int)]) (Maybe (TT Name, [(Name, TT Name)], Stack))
+>     match (Sch pats _ rhs) xs env patvars 
+>               = matchargs pats xs rhs env patvars []
+>     matchargs [] xs (Ind rhs) env patvars pv' = return $ Just (rhs, pv', xs)
+>     matchargs (p:ps) (x:xs) rhs env patvars pv'
+>               = do x' <- (eval x [] env patvars) 
+>                    case matchPat p x' pv' of
+>                      Just patvars' -> matchargs ps xs rhs env patvars patvars'
+>                      Nothing -> return Nothing
+>     matchargs _ _ _ _ _ _ = return Nothing
 
 >     matchPat PTerm x patvars = Just patvars
->     matchPat (PVar n) x patvars = Just ((n,x):patvars)
+>     matchPat (PVar n) x patvars = Just ((n,x):patvars) -- (filter (\ (x,y) -> x/=n) patvars))
 >     matchPat (PConst t) (Const t') patvars
 >                  = do tc <- cast t
 >                       if (tc == t') then Just patvars
@@ -134,3 +203,25 @@
 >     getConArgs (Con t _ _) args = Just (t, args)
 >     getConArgs (App f a) args = getConArgs f (a:args)
 >     getConArgs _ _ = Nothing
+
+
+
+> eval_nfEnv :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name
+> eval_nfEnv env g t
+>     = eval_nf (addenv env g) t
+>   where addenv [] g = g
+>         addenv ((n,B (Let v) ty):xs) (Gam g)
+>             = addenv xs (Gam (Map.insert n (G (Fun [] (Ind v)) (Ind ty) defplicit) g))
+>         addenv (_:xs) g = addenv xs g
+
+Turn MN to UN, if they are unique, so that they look nicer.
+
+> tidyNames :: Indexed Name -> Indexed Name
+> tidyNames (Ind tm) = Ind (tidy' [] tm)
+>   where tidy' ns (Bind (MN (n,i)) (B b t) (Sc tm)) = 
+>             let n' = uniqify (UN n) ns in
+>                 Bind n' (B b (tidy' ns t)) (Sc (tidy' (n':ns) tm))
+>         tidy' ns (Bind x (B b t) (Sc tm)) 
+>               = Bind x (B b (tidy' ns t)) (Sc (tidy' (x:ns) tm))
+>         tidy' ns (App f a) = App (tidy' ns f) (tidy' ns a)
+>         tidy' ns x = x
diff --git a/Ivor/ICompile.lhs b/Ivor/ICompile.lhs
--- a/Ivor/ICompile.lhs
+++ b/Ivor/ICompile.lhs
@@ -1,9 +1,12 @@
+FIXME: I don't believe this is used. Make it go away.
+
 > module Ivor.ICompile where
 
 > import Ivor.TTCore
 > import Ivor.Datatype
 > import Ivor.Nobby
 > import Ivor.Gadgets
+> import Ivor.Values
 
 > import Data.List
 > import Debug.Trace
@@ -31,8 +34,8 @@
 >			 let top = map schhead ss'
 >			     rest = map schtail ss' in
 >			 icomp' top rest es'
->          schhead (Sch x red) = (head x, red)
->          schtail (Sch x red) = Sch (tail x) red
+>          schhead (Sch x bs red) = (head x, red)
+>          schtail (Sch x bs red) = Sch (tail x) bs red
 >          icomp' x xs (e:es) | allDisjoint (map fst x) = doCase1 e x
 >		              | otherwise = error "Can't find a scrutinee"
 >          orderPatts = sortBy cmpPat
@@ -43,7 +46,7 @@
 > mangleArgOrder :: [Scheme Name] -> [Int] -> [Scheme Name]
 > mangleArgOrder [] _ = []
 > mangleArgOrder (x:xs) es = (ma' x es):(mangleArgOrder xs es)
->    where ma' (Sch ps ired) es = Sch (reorder ps es) ired
+>    where ma' (Sch ps bs ired) es = Sch (reorder ps es) bs ired
 >          reorder ps xs = foldl (\ih x -> (ps!!x):ih) [] xs
 
 > allDisjoint ps = numDisjoint ps == length ps
diff --git a/Ivor/Nobby.lhs b/Ivor/Nobby.lhs
--- a/Ivor/Nobby.lhs
+++ b/Ivor/Nobby.lhs
@@ -5,6 +5,7 @@
 > import Ivor.TTCore
 > import Ivor.Gadgets
 > import Ivor.Constant
+> import Ivor.Values
 
 > import Data.List
 > import Control.Monad
@@ -13,200 +14,6 @@
 
 > import Debug.Trace
 
-To begin, we need to define the context in which normalisation takes place.
-The context maps names to user defined functions, constructors and
-elimination rules.
-
-Global represents all possible global names --- if it's a user defined
-name, hold its definition, otherwise hold what it is so we know what
-to do with it, when the time comes.
-
-> data Global n
->     = Fun [FunOptions] (Indexed n)    -- User defined function
->     | Partial (Indexed n) [n] -- Unfinished definition
->     | PatternDef (PMFun n) Bool -- Pattern matching definition, totality
->     | ElimRule ElimRule  -- Elimination Rule
->     | PrimOp PrimOp EvPrim     -- Primitive function
->     | DCon Int Int       -- Data Constructor, tag and arity
->     | TCon Int (Elims n) -- Type Constructor and arity, elim rule name
->     | Unreducible        -- Unreducible name
->     | Undefined          -- Declared but undefined name
-
-> data Elims n = Elims { elimRuleName :: n,
->                        caseRuleName :: n,
->                        constructors :: [n] }
->              | NoConstructorsYet
-
-> data FunOptions = Frozen | Recursive | Total
->   deriving Eq
-
-> instance Show n => Show (Global n) where
->     show (Fun opts t) = "Fun " ++ show t
->     show (ElimRule _) = "<<elim rule>>"
->     show (PrimOp _ _) = "<<primitive operator>>"
->     show (DCon x t) = "DCon " ++ show x ++ "," ++show t
->     show (TCon x (Elims e c cons)) = "TCon " ++ show x
->     show Unreducible = "Unreducible"
->     show Undefined = "Undefined"
-
-> type Plicity = Int
-
-> defplicit = 0
-
-> data Ord n => Gval n = G (Global n) (Indexed n) Plicity
->    deriving Show
-
-> getglob (G v t p) = v
-> gettype (G v t p) = t
-> getplicity (G v t p) = p
-
-> newtype Ord n => Gamma n = Gam (Map.Map n (Gval n))
->     deriving Show
-
-> extend (Gam x) (n,v) = Gam (Map.insert n v x)
-
-> emptyGam :: Ord n => Gamma n
-> emptyGam = Gam Map.empty
-
-> getAList :: Ord n => Gamma n -> [(n,(Gval n))]
-> getAList (Gam n) = Map.toAscList n
-
-> lookupval :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Global n)
-> lookupval n (Gam xs) = fmap getglob (Map.lookup n xs)
-
-> lookuptype :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Indexed n)
-> lookuptype n (Gam xs) = fmap gettype (Map.lookup n xs)
-
-> glookup ::  (Ord n, Eq n) => n -> Gamma n -> Maybe (Global n,Indexed n)
-> glookup n (Gam xs) = fmap (\x -> (getglob x,gettype x)) (Map.lookup n xs)
-
-Get a type name from the context
-
-> getTyName :: Monad m => Gamma Name -> Name -> m Name
-> getTyName  gam n = case lookuptype n gam of
->                            Just (Ind ty) -> return $ getFnName ty
->                            Nothing -> fail $ "No such name " ++ show n
->   where getFnName (TyCon x _) = x
->         getFnName (App f x) = getFnName f
->         getFnName (Bind _ _ (Sc x)) = getFnName x
->         getFnName x = MN ("Dunno: "++show x, 0)
-
-Return whether a name is a recursive constructor (i.e, its family name
-occurs anywhere in its arguments).
-
-> recCon :: Name -> Gamma Name -> Bool
-> recCon n gam = case glookup n gam of
->                  (Just (DCon _ t, Ind ty)) ->
->                      checkRec (conFamily ty) (map snd (getExpected ty))
->                  _ -> False
->    where conFamily t = fname (getFun (getReturnType t))
->          fname (TyCon n _) = n
->          fname _ = MN ("ERROR!",0)
->          checkRec n [] = False
->          checkRec n (x:xs) = nameOccurs n (forget x) || checkRec n xs
-
-> insertGam :: Ord n => n -> Gval n -> Gamma n -> Gamma n
-> insertGam nm val (Gam gam) = Gam $ Map.insert nm val gam
-
-> concatGam :: Ord n => Gamma n -> Gamma n -> Gamma n
-> concatGam (Gam x) (Gam y) = Gam (Map.union x y)
-
-> setFrozen :: (Ord n, Eq n) => n -> Bool -> Gamma n -> Gamma n
-> setFrozen n freeze (Gam xs) = Gam $ Map.mapWithKey sf xs where
->    sf p (G (Fun opts v) ty plicit)
->        | n == p = (G (Fun (doFreeze freeze opts) v) ty plicit)
->    sf _ x = x
->    doFreeze True opts = nub (Frozen:opts)
->    doFreeze False opts = opts \\ [Frozen]
-
-> setRec :: (Ord n, Eq n) => n -> Bool -> Gamma n -> Gamma n
-> setRec n frec (Gam xs) = Gam $ Map.mapWithKey sf xs where
->    sf p (G (Fun opts v) ty plicit)
->        | n == p = (G (Fun (doFrec frec opts) v) ty plicit)
->    sf _ x = x
->    doFrec True opts = nub (Recursive:opts)
->    doFrec False opts = opts \\ [Recursive]
-
-
-> freeze :: (Ord n, Eq n) => n -> Gamma n -> Gamma n
-> freeze n gam = setFrozen n True gam
-
-> thaw :: (Ord n, Eq n) => n -> Gamma n -> Gamma n
-> thaw n gam = setFrozen n False gam
-
-Remove a name from the middle of the context - should only be valid
-if it's a partial definition or an axiom which is about to be replaced.
-
-> remove :: (Ord n, Eq n) => n -> Gamma n -> Gamma n
-> remove n (Gam xs) = Gam $ Map.delete n xs
-
-Insert a name into the context. If the name is already there, this
-is an error *unless* the old definition was 'Undefined', in which case
-the name is replaced.
-
-> gInsert :: (Monad m, Ord n, Eq n, Show n) => 
->            n -> Gval n -> Gamma n -> m (Gamma n)
-> gInsert nm val (Gam xs) = case Map.lookup nm xs of
->         -- FIXME: Check ty against val
->       Nothing -> return $ Gam (Map.insert nm val xs)
->       Just (G Undefined ty _) -> return $ Gam (Map.insert nm val xs)
->       Just (G (TCon _ NoConstructorsYet) ty _) -> 
->                                  return $ Gam (Map.insert nm val xs)
->       Just _ -> fail $ "Name " ++ show nm ++ " is already defined"
-
-An ElimRule is a Haskell implementation of the iota reductions of
-a family.
-
-> type ElimRule = Spine Value -> Maybe Value
-
-A PrimOp is an external operation
-
-> type PrimOp = Spine Value -> Maybe Value
-> type EvPrim = [TT Name] -> Maybe (TT Name) -- same, but with tt terms rather than values
-
-Model represents normal forms, including Ready (reducible) and Blocked
-(non-reducible) forms.
-
-> data Model s = MR (Ready s)
->              | MB (Blocked s, Model s) (Spine (Model s))
-
-> data Ready s
->     = RdBind Name (Binder (Model s)) (s (Model s))
->     | RCon Int Name (Spine (Model s))
->     | RTyCon Name (Spine (Model s))
->     | forall c. Constant c => RdConst c
->     | RdStar
->     | RdLabel (Model s) (MComp s)
->     | RdCall (MComp s) (Model s)
->     | RdReturn (Model s)
->     | RdCode (Model s)
->     | RdQuote (Model s) -- (TT Name)
->     | RdInfer
-
-> data Blocked s
->     = BCon Int Name Int
->     | BTyCon Name Int
->     | BElim ElimRule Name
->     | BPatDef (PMFun Name) Name
->     | BPrimOp PrimOp Name
->     | BRec Name Value
->     | BP Name
->     | BV Int
->     | BEval (Model s) (Model s)
->     | BEscape (Model s) (Model s)
-
-> data MComp s = MComp Name [Model s]
-
-> newtype Weakening = Wk Int
-
-Second weakening is cached to prevent function composition in the weaken
-class.
-
-> newtype Kripke x = Kr (Weakening -> x -> x, Weakening)
-
-> type Value = Model Kripke
-> type Normal = Model Scope
-
 > newtype Ctxt = VG [Value]
 
 > type PatVals = [(Name, Value)]
@@ -240,11 +47,11 @@
 >           Nothing -> evalP (lookupval n gamma)
 >    where evalP (Just Unreducible) = (MB (BP n,pty n) Empty)
 >          evalP (Just Undefined) = (MB (BP n, pty n) Empty)
->          evalP (Just (PatternDef p@(PMFun 0 pats) _)) =
+>          evalP (Just (PatternDef p@(PMFun 0 pats) _ _)) =
 >              case patmatch gamma g pats [] of
 >                 Nothing ->  (MB (BPatDef p n, pty n) Empty)
 >                 Just v -> v
->          evalP (Just (PatternDef p _)) = (MB (BPatDef p n, pty n) Empty)
+>          evalP (Just (PatternDef p _ _)) = (MB (BPatDef p n, pty n) Empty)
 >          evalP (Just (Partial (Ind v) _)) = (MB (BP n, pty n) Empty)
 >          evalP (Just (PrimOp f _)) = (MB (BPrimOp f n, pty n) Empty)
 >          evalP (Just (Fun opts (Ind v)))
@@ -361,7 +168,7 @@
 
 > patmatch :: Gamma Name -> Ctxt -> [PMDef Name] -> [Value] -> Maybe Value
 > patmatch gam g [] _ = Nothing
-> patmatch gam g ((Sch pats ret):ps) vs = case pm gam g pats vs ret [] of
+> patmatch gam g ((Sch pats _ ret):ps) vs = case pm gam g pats vs ret [] of
 >                         Nothing -> patmatch gam g ps vs
 >                         Just v -> Just v
 
diff --git a/Ivor/PatternDefs.lhs b/Ivor/PatternDefs.lhs
--- a/Ivor/PatternDefs.lhs
+++ b/Ivor/PatternDefs.lhs
@@ -8,6 +8,7 @@
 > import Ivor.Typecheck
 > import Ivor.Unify
 > import Ivor.Errors
+> import Ivor.Values
 
 > import Debug.Trace
 > import Data.List
@@ -31,6 +32,7 @@
 >   let clauses = nub (concat clausesIn)
 >   let clauses' = filter (mostSpecClause clauses) clauses
 >   (ty@(Ind ty'),_) <- typecheck gam tyin
+>   checkRealNames (getNames (Sc ty')) ty
 >   let arity = length (getExpected ty')
 >   checkNotExists fn gam
 >   gam' <- gInsert fn (G Undefined ty defplicit) gam
@@ -85,7 +87,7 @@
 
 Check for definition 1 above: one argument position is well founded
 
->         wfClause args (Sch pats (Ind t)) = do
+>         wfClause args (Sch pats _ (Ind t)) = do
 >            let recs = findRec [] t
 >            case recs of
 >               [] -> return args
@@ -94,7 +96,7 @@
 Check for definition 2 above: all recursive calls have a decreasing argument
 and no increasing arguments
 
->         allDec (Sch pats (Ind t)) err = do
+>         allDec (Sch pats _ (Ind t)) err = do
 >            let recs = findRec [] t
 >            case allRecDec pats recs of
 >              Success v -> return v
@@ -214,33 +216,47 @@
 >                let namesret = filter (notGlobal gam') $ getNames (Sc rtmtt')
 >                let namesbound = getNames (Sc tmtt)
 >                checkAllBound (fileLine ret) namesret namesbound (Ind rtmtt') tmtt rty pty
->                -- trace (show (unified, rtmtt, tm, rtmtt')) $ 
->                return ((tm, Ind rtmtt', newdefs), [], newdefs, True)
->         mytypecheck gam (clause, (RWith scr pats)) i =
+>                -- trace (show env) $
+>                return ((tm, Ind rtmtt', env), [], newdefs, True)
+>         mytypecheck gam (clause, (RWith addprf scr pats)) i =
 >             do -- Get the type of scrutinee, construct the type of the auxiliary definition
 >                (tm@(Ind clausett), clausety, _, scrty@(Ind stt), env) <- checkAndBindWith gam clause scr fn
 >                let args = getRawArgs clause
->                let restTyin = addLastArg tyin (forget scrty)
+>                -- let restTyin = addLastArg tyin (forget scrty) scr
 >                margs <- getMatches tm tm
 >                let margNames = nub (map fst margs)
 >                let newargs = filter (\ (x,ty) -> x `elem` margNames) env
 >                newpats <- mapM (getNewPat tm 1) pats
->                let newfntyin = mkNewTy (newargs ++ [(UN "__scr", B Pi stt)]) clausety
->                (newfnTy, _) <- check gam env (forget newfntyin) (Just (Ind Star))
+>                let newfntyin = forget (mkNewTy newargs clausety)
+>                let newfntyin' = addLastArg newfntyin (forget stt) scr addprf
+>                   --(newargs ++ [(UN "__scr", B Pi stt),
+>                   --                                (UN "__scrEq", B Pi (screq (UN "__scr") scr))]) clausety
+>                (newfnTy, _) <- check gam env newfntyin' (Just (Ind Star))
 >                -- Make a name for the new function, clauses in 'pats' need the new name,
 >                -- and form a definition of type restTy
 >                let newname = mkNewName fn i
 >                -- TODO: All pats have to match against args ++ [_]
->                -- Final clause returns newname applied to args++scrutinee
->                let ret = rawApp (Var newname) ((map Var (map fst newargs)) ++ [scr])
+>                -- Final clause returns newname applied to args++scrutinee++refl
+>                let ret = rawApp (Var newname) ((map Var (map fst newargs)) ++ 
+>                              [scr] ++ if addprf then 
+>                                           [RApp (RApp (Var (UN "refl")) RInfer) RInfer]
+>                                          else [])
 >                let gam' = insertGam newname (G Undefined newfnTy 0) gam
->                newpdef <- mapM (newp tm newargs 1) (zip newpats pats)
+>                newpdef <- mapM (newp tm newargs 1 addprf) (zip newpats pats)
 >                (chk, auxdefs, _, _) <- mytypecheck gam' (clause, (RWRet ret)) i
 >                (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover
 >                return (chk, auxdefs++auxdefs', newdefs, covers)
 
->         addLastArg (RBind n (B Pi arg) x) ty = RBind n (B Pi arg) (addLastArg x ty)
->         addLastArg x ty = RBind (UN "X") (B Pi ty) x
+>         addLastArg (RBind n (B Pi arg) x) ty scr addprf 
+>                        = RBind n (B Pi arg) (addLastArg x ty scr addprf)
+>         addLastArg x ty scr addprf 
+>            = RBind (UN "__scr") (B Pi ty) 
+>                 (if addprf then (RBind (UN "__scrEq") (B Pi (screq (UN "__scr") scr)) x)
+>                     else x)
+
+>         screq scrname scr = RApp (RApp (RApp (RApp (Var (UN "Eq")) RInfer) RInfer)
+>                                scr) (Var scrname)
+
 >         rawApp f [] = f
 >         rawApp f (a:as) = rawApp (RApp f a) as
 
@@ -255,13 +271,14 @@
 >             (argv, argt, _) <- checkAndBind gam [] pargs Nothing
 >             getMatches argv proto
 
->         newp proto newargs i (newps, RSch args ret) = do
+>         newp proto newargs i addprf (newps, RSch args ret) = do
 >             ret' <- newpRet ret
->             return $ RSch ((getAuxPats (map fst newargs) newps)++(lastn i args)) ret'
->                 where newpRet (RWith v schs) = 
+>             return $ RSch ((getAuxPats (map fst newargs) newps)++(lastn i args) ++
+>                              (if addprf then [RInfer] else [])) ret'
+>                 where newpRet (RWith prf v schs) = 
 >                          do newpats <- mapM (getNewPat proto (i+1)) schs
->                             newpdef <- mapM (newp proto newargs (i+1)) (zip newpats schs)
->                             return (RWith v newpdef)
+>                             newpdef <- mapM (newp proto newargs (i+1) prf) (zip newpats schs)
+>                             return (RWith prf v newpdef)
 >                       newpRet r = return r
 
 >         lastn i xs = reverse $ take i (reverse xs)
@@ -282,7 +299,7 @@
 >         addContext (Just (f,l)) err = IContext (f ++ ":" ++ show l ++ ":") err
 
 > mkScheme :: Gamma Name -> (Indexed Name, Indexed Name) -> PMDef Name
-> mkScheme gam (Ind pat, ret) = Sch (map mkpat (getPatArgs pat)) ret
+> mkScheme gam (Ind pat, ret) = Sch (map mkpat (getPatArgs pat)) [] ret
 >   where mkpat (P n) = PVar n
 >         mkpat (App f a) = addPatArg (mkpat f) (mkpat a)
 >         mkpat (Con i nm ar) = mkPatV nm (lookupval nm gam)
diff --git a/Ivor/RunTT.lhs b/Ivor/RunTT.lhs
--- a/Ivor/RunTT.lhs
+++ b/Ivor/RunTT.lhs
@@ -2,6 +2,8 @@
 
 > module Ivor.RunTT where
 
+FIXME: We don't use this. Got to go.
+
 Representation of the run-time language.
 Used for spitting out GHC core.
 
@@ -9,6 +11,7 @@
 > import Ivor.Gadgets
 > import Ivor.ICompile
 > import Ivor.Nobby
+> import Ivor.Values
 
 When we compile, we need to know the term as well as bits of info about
 its type, ie its arity and emptiness.
diff --git a/Ivor/Scopecheck.lhs b/Ivor/Scopecheck.lhs
--- a/Ivor/Scopecheck.lhs
+++ b/Ivor/Scopecheck.lhs
@@ -5,6 +5,7 @@
 > import Ivor.TTCore
 > import Ivor.Nobby
 > import Ivor.Typecheck
+> import Ivor.Values
 
 Typechecking on terms we assume to be okay - in other words, just convert 
 bound names to a de Bruijn index.
diff --git a/Ivor/Shell.lhs b/Ivor/Shell.lhs
--- a/Ivor/Shell.lhs
+++ b/Ivor/Shell.lhs
@@ -158,9 +158,9 @@
 >                         (Name DataCon _) -> return (respondLn st "Data constructor")
 >                         _ -> fail "Unknown definition"
 >     where printPats (Patterns cs) = unlines (map printClause cs)
->           printClause (PClause args ret) = n ++ " " ++
->                                            unwords (map argshow args) ++
->                                            " = " ++ show ret
+>           printClause (PClause args _ ret) = n ++ " " ++
+>                                              unwords (map argshow args) ++
+>                                              " = " ++ show ret
 >           argshow x | ' ' `elem` show x = "(" ++ show x ++ ")"
 >                     | otherwise = show x
 
diff --git a/Ivor/ShellParser.lhs b/Ivor/ShellParser.lhs
--- a/Ivor/ShellParser.lhs
+++ b/Ivor/ShellParser.lhs
@@ -131,7 +131,7 @@
 > pclauseret :: [ViewTerm] -> Maybe (Parser ViewTerm) -> Parser PClause
 > pclauseret args ext = do lchar '='
 >                          ret <- pTerm ext
->                          return $ PClause args ret
+>                          return $ PClause args [] ret
 
 > pclausewith :: String -> [ViewTerm] -> Maybe (Parser ViewTerm) -> Parser PClause
 > pclausewith nm args ext = do lchar '|'
@@ -139,7 +139,7 @@
 >                              lchar '{'
 >                              pats <- ppatterns nm ext
 >                              lchar '}'
->                              return $ PWithClause args scr pats
+>                              return $ PWithClause False args scr pats
 
 > ppatterns :: String -> Maybe (Parser ViewTerm) -> Parser Patterns
 > ppatterns name ext
diff --git a/Ivor/State.lhs b/Ivor/State.lhs
--- a/Ivor/State.lhs
+++ b/Ivor/State.lhs
@@ -1,4 +1,4 @@
-> {-# OPTIONS_GHC -fglasgow-exts #-}
+\> {-# OPTIONS_GHC -fglasgow-exts #-}
 
 > module Ivor.State where
 
@@ -17,6 +17,7 @@
 > import Ivor.Display
 > import Ivor.Unify
 > import Ivor.Errors
+> import Ivor.Values
 
 > import System.Environment
 > import Data.List
@@ -107,7 +108,7 @@
 >              gInsert n gl ctxt
 >          addElim ctxt erule schemes = do
 >            newdefs <- gInsert (fst erule)
->                               (G (PatternDef schemes True) (snd erule) defplicit)
+>                               (G (PatternDef schemes True False) (snd erule) defplicit)
 >                               ctxt
 >            return newdefs
 
diff --git a/Ivor/TT.lhs b/Ivor/TT.lhs
--- a/Ivor/TT.lhs
+++ b/Ivor/TT.lhs
@@ -35,8 +35,8 @@
 >               proofterm, getGoals, getGoal, uniqueName, -- getActions
 >               allSolved,qed,
 >               -- * Examining the Context
->               eval, whnf, evalnew, evalCtxt, getDef, defined, getPatternDef,
->               getAllTypes, getAllDefs, getAllPatternDefs, getConstructors,
+>               eval, whnf, evalnew, evalnewWithout, evalnewLimit, evalCtxt, getDef, defined, getPatternDef,
+>               getAllTypes, getAllDefs, getAllPatternDefs, isAuxPattern, getConstructors,
 >               getInductive, getAllInductives, getType,
 >               Rule(..), getElimRule, nameType, getConstructorTag,
 >               getConstructorArity,
@@ -113,6 +113,7 @@
 > import Ivor.CodegenC
 > import Ivor.PatternDefs
 > import Ivor.Errors
+> import Ivor.Values
 
 > import Data.List
 > import Debug.Trace
@@ -188,6 +189,7 @@
 >              | Message String
 >              | Unbound ViewTerm ViewTerm ViewTerm ViewTerm [Name]
 >              | NoSuchVar Name
+>              | CantInfer Name ViewTerm
 >              | ErrContext String TTError
 
 > instance Show TTError where
@@ -197,6 +199,7 @@
 >     show (Unbound clause clty rhs rhsty ns) 
 >        = show ns ++ " unbound in clause " ++ show clause ++ " : " ++ show clty ++ 
 >                     " = " ++ show rhs
+>     show (CantInfer  n tm) = "Can't infer value for " ++ show n ++ " in " ++ show tm
 >     show (NoSuchVar n) = "No such name as " ++ show n
 >     show (ErrContext c err) = c ++ show err
 
@@ -223,6 +226,7 @@
 >                        (view (Term (rhs, Ind TTCore.Star)))
 >                        (view (Term (rhsty, Ind TTCore.Star)))
 >                        names
+> getError (ICantInfer nm tm) = CantInfer nm (view (Term (tm, Ind TTCore.Star)))
 > getError (INoSuchVar n) = NoSuchVar n
 > getError (IContext s e) = ErrContext s (getError e)
 
@@ -263,9 +267,11 @@
 
 > data PClause = PClause {
 >                         arguments :: [ViewTerm],
+>                         boundnames :: [(Name, ViewTerm)],
 >                         returnval :: ViewTerm
 >                        }
 >              | PWithClause {
+>                         eqproof :: Bool,
 >                         arguments :: [ViewTerm],
 >                         scrutinee :: ViewTerm,
 >                         patterns :: Patterns
@@ -276,10 +282,10 @@
 >    deriving Show
 
 > mkRawClause :: PClause -> RawScheme
-> mkRawClause (PClause args ret) =
+> mkRawClause (PClause args _ ret) =
 >     RSch (map forget args) (RWRet (forget ret))
-> mkRawClause (PWithClause args scr (Patterns rest)) = 
->     RSch (map forget args) (RWith (forget scr) (map mkRawClause rest))
+> mkRawClause (PWithClause prf args scr (Patterns rest)) = 
+>     RSch (map forget args) (RWith prf (forget scr) (map mkRawClause rest))
 
 > -- ^ Convert a term to matchable pattern form; i.e. the only names allowed
 > -- are variables and constructors. Any arbitrary function application is
@@ -339,8 +345,9 @@
 >         return (Ctxt st { defs = newdefs }, vnewnames)
 >   where insertAll [] gam tot = return gam
 >         insertAll ((nm, def, ty):xs) gam tot = 
->             do gam' <- gInsert nm (G (PatternDef def tot) ty defplicit) gam
+>             do gam' <- gInsert nm (G (PatternDef def tot (gen nm)) ty defplicit) gam
 >                insertAll xs gam' tot
+>         gen nm = nm /= n -- generated if it's not the provided name.
 
 > -- |Add a new definition, with its type to the global state.
 > -- These definitions can be recursive, so use with care.
@@ -480,8 +487,9 @@
 >        t <- raw tm
 >        let Gam ctxt = defs st
 >        case (typecheck (defs st) t) of
->           (Right (t, ty)) ->
->              do tt $ checkConv (defs st) ty (Ind TTCore.Star) (IMessage "Not a type")
+>           (Right (t@(Ind t'), ty)) ->
+>              do tt $ checkRealNames (getNames (Sc t')) t
+>                 tt $ checkConv (defs st) ty (Ind TTCore.Star) (IMessage "Not a type")
 >                 -- let newdefs = Gam ((n, (G und (finalise t))):ctxt)
 >                 newdefs <- gInsert n (G und (finalise t) defplicit) (Gam ctxt)
 >                 return $ Ctxt st { defs = newdefs }
@@ -704,9 +712,9 @@
 > resume :: Context -> Name -> TTM Context
 > resume ctxt@(Ctxt st) n =
 >     case glookup n (defs st) of
->         Just ((Ivor.Nobby.Partial _ _),_) -> do let (Ctxt st) = suspend ctxt
->                                                 st' <- tt$ resumeProof st n
->                                                 return (Ctxt st')
+>         Just ((Ivor.Values.Partial _ _),_) -> do let (Ctxt st) = suspend ctxt
+>                                                  st' <- tt$ resumeProof st n
+>                                                  return (Ctxt st')
 >         Just (Unreducible,ty) ->
 >             do let st' = st { defs = remove n (defs st) }
 >                theorem (Ctxt st') n (Term (ty, Ind TTCore.Star))
@@ -721,7 +729,7 @@
 > freeze (Ctxt st) n
 >      = case glookup n (defs st) of
 >           Nothing -> fail $ show n ++ " is not defined"
->           _ -> return $ Ctxt st { defs = Ivor.Nobby.freeze n (defs st) }
+>           _ -> return $ Ctxt st { defs = Ivor.Values.freeze n (defs st) }
 
 > -- | Unfreeze a name (i.e., allow it to reduce).
 > -- Fails if the name does not exist.
@@ -729,7 +737,7 @@
 > thaw (Ctxt st) n
 >      = case glookup n (defs st) of
 >           Nothing -> fail $ show n ++ " is not defined"
->           _ -> return $ Ctxt st { defs = Ivor.Nobby.thaw n (defs st) }
+>           _ -> return $ Ctxt st { defs = Ivor.Values.thaw n (defs st) }
 
 
 > -- | Save the state (e.g. for Undo)
@@ -773,9 +781,21 @@
 
 > -- |Reduce a term and its type to Normal Form (using new evaluator)
 > evalnew :: Context -> Term -> Term
-> evalnew (Ctxt st) (Term (tm,ty)) = Term (eval_nf (defs st) tm,
->                                          eval_nf (defs st) ty)
+> evalnew (Ctxt st) (Term (tm,ty)) = Term (tidyNames (eval_nf (defs st) tm),
+>                                          tidyNames (eval_nf (defs st) ty))
 
+> -- |Reduce a term and its type to Normal Form (using new evaluator, not
+> -- reducing given names)
+> evalnewWithout :: Context -> Term -> [Name] -> Term
+> evalnewWithout (Ctxt st) (Term (tm,ty)) ns = Term (tidyNames (eval_nf_without (defs st) tm ns),
+>                                                    tidyNames (eval_nf_without (defs st) ty ns))
+
+> -- |Reduce a term and its type to Normal Form (using new evaluator, reducing
+> -- given names a maximum number of times)
+> evalnewLimit :: Context -> Term -> [(Name, Int)] -> Term
+> evalnewLimit (Ctxt st) (Term (tm,ty)) ns = Term (eval_nf_limit (defs st) tm ns,
+>                                                  eval_nf_limit (defs st) ty ns)
+
 > -- |Check a term in the context of the given goal
 > checkCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term
 > checkCtxt (Ctxt st) goal tm =
@@ -877,7 +897,7 @@
 > getPatternDef :: Context -> Name -> TTM (ViewTerm, Patterns)
 > getPatternDef (Ctxt st) n
 >     = case glookup n (defs st) of
->           Just ((PatternDef pmf _),ty) ->
+>           Just ((PatternDef pmf _ _),ty) ->
 >               return $ (view (Term (ty, Ind TTCore.Star)), 
 >                         Patterns (map mkPat (getPats pmf)))
 >           Just ((Fun _ ind), ty) ->
@@ -885,8 +905,12 @@
 >                         Patterns [mkCAFpat ind])
 >           _ -> fail "Not a pattern matching definition"
 >    where getPats (PMFun _ ps) = ps
->          mkPat (Sch ps ret) = PClause (map viewPat ps) (view (Term (ret, (Ind TTCore.Star))))
->          mkCAFpat tm = PClause [] (view (Term (tm, (Ind TTCore.Star))))
+>          mkPat (Sch ps bs ret) 
+>               = PClause (map viewPat ps) 
+>                         (map (\ (n, B _ t) -> 
+>                            (n, (view (Term (Ind t, (Ind TTCore.Star)))))) bs)
+>                 (view (Term (ret, (Ind TTCore.Star))))
+>          mkCAFpat tm = PClause [] [] (view (Term (tm, (Ind TTCore.Star))))
 >          viewPat (PVar n) = Name Bound n --(name (show n))
 >          viewPat (PCon t n ty ts) = VTerm.apply (Name Bound (name (show n))) (map viewPat ts)
 >          viewPat (PConst c) = Constant c
@@ -908,6 +932,14 @@
 >                          Right d -> (x,d):(getPD xs)
 >                          _ -> getPD xs
 
+> -- |Is the name an auxiliary function of a pattern definition (e.g. generated by a with
+> -- clause?
+> isAuxPattern :: Context -> Name -> Bool
+> isAuxPattern (Ctxt st) n = case glookup n (defs st) of
+>           Just ((PatternDef pmf _ gen),ty) -> gen
+>           _ -> False
+
+
 > -- |Get all the inductive type definitions in the context.
 > getAllInductives :: Context -> [(Name,Inductive)]
 > getAllInductives ctxt 
@@ -971,7 +1003,7 @@
 >             elim <- lookupM rule (eliminators st)
 >             return $ Patterns $ map mkRed (fst $ snd elim)
 >       Nothing -> fail $ (show nm) ++ " is not a type constructor"
->  where mkRed (RSch pats (RWRet ret)) = PClause (map viewRaw pats) (viewRaw ret)
+>  where mkRed (RSch pats (RWRet ret)) = PClause (map viewRaw pats) [] (viewRaw ret)
 >         -- a reduction will only have variables and applications
 >        viewRaw (Var n) = Name Free n
 >        viewRaw (RApp f a) = VTerm.App (viewRaw f) (viewRaw a)
diff --git a/Ivor/TTCore.lhs b/Ivor/TTCore.lhs
--- a/Ivor/TTCore.lhs
+++ b/Ivor/TTCore.lhs
@@ -9,6 +9,7 @@
 > import Data.Char
 > import Control.Monad.State
 > import Data.Typeable
+> import Data.Binary hiding (get,put)
 > import Debug.Trace
 
 Raw terms are those read in directly from the user, and may be badly typed.
@@ -149,8 +150,8 @@
 
 Data declarations and pattern matching
 
-> data RawWith = RWith Raw [RawScheme] -- match with an extra arg, add new schemes
->              | RWRet Raw
+> data RawWith = RWith Bool Raw [RawScheme] -- match with an extra arg, add new schemes
+>              | RWRet Raw                  -- if Bool is true, add an equality proof
 >   deriving Show
 
  data With = With [Indexed n]
@@ -161,7 +162,7 @@
 > data RawScheme = RSch [Raw] RawWith
 >   deriving Show
 
-> data Scheme n = Sch [Pattern n] {- With -} (Indexed n)
+> data Scheme n = Sch [Pattern n] (Env n) (Indexed n)
 >         deriving Show
 
 > type PMRaw = RawScheme
@@ -742,6 +743,7 @@
 >       fPrec _ (RInfer) = "_"
 >       fPrec _ (RMeta n) = "?"++forget n
 >       fPrec p (RFileLoc f l t) = fPrec p t
+>       fPrec p (RAnnot s) = "[" ++ s ++ "]"
 >       bracket outer inner str | inner>outer = "("++str++")"
 >                               | otherwise = str
 
@@ -940,3 +942,32 @@
 >        forgetTT (Stage (Escape t _)) = RStage (REscape (forgetTT t))
 >        forgetTT (Const x) = RConst x
 >        forgetTT Star = RStar
+
+> pToV :: Eq n => n -> (TT n) -> (Scope (TT n))
+> pToV = pToV2 0
+
+> pToV2 v p (P n) | p==n = Sc (V v)
+>                 | otherwise = Sc (P n)
+> pToV2 v p (V w) = Sc (V w)
+> pToV2 v p (Con t n i) = Sc (Con t n i)
+> pToV2 v p (TyCon n i) = Sc (TyCon n i)
+> pToV2 v p (Meta n t) = Sc (Meta n (getSc (pToV2 v p t)))
+>				where getSc (Sc a) = a
+> pToV2 v p (Elim n) = Sc (Elim n)
+> pToV2 v p (Bind n b (Sc sc)) = Sc (Bind n (fmap (getSc.(pToV2 v p)) b)
+>                                    (pToV2 (v+1) p sc))
+>				where getSc (Sc a) = a
+> pToV2 v p (App f a) = Sc $ App (getSc (pToV2 v p f))
+>                               (getSc (pToV2 v p a))
+>				where getSc (Sc a) = a
+> pToV2 v p (Label t (Comp n ts)) = Sc $ Label (getSc (pToV2 v p t))
+>                                         (Comp n (map (getSc.(pToV2 v p)) ts))
+> pToV2 v p (Call (Comp n ts) t) = Sc $ Call 
+>                                        (Comp n (map (getSc.(pToV2 v p)) ts))
+>                                        (getSc (pToV2 v p t))
+> pToV2 v p (Return t) = Sc $ Return (getSc (pToV2 v p t))
+> pToV2 v p (Proj n i t) = Sc $ Proj n i (getSc (pToV2 v p t))
+>				where getSc (Sc a) = a
+> pToV2 v p (Stage t) = Sc $ Stage (sLift (getSc.(pToV2 v p)) t)
+> pToV2 v p (Const x) = Sc (Const x)
+> pToV2 v p Star = Sc Star
diff --git a/Ivor/Tactics.lhs b/Ivor/Tactics.lhs
--- a/Ivor/Tactics.lhs
+++ b/Ivor/Tactics.lhs
@@ -8,6 +8,7 @@
 > import Ivor.Gadgets
 > import Ivor.Unify
 > import Ivor.Errors
+> import Ivor.Values
 
 > import Data.List
 > import Data.Maybe
@@ -471,9 +472,10 @@
 
 > casetac :: Bool -> Raw -> Tactic
 > casetac rec scrutinee gam env tm@(Ind (Bind x (B Hole ty) sc)) =
->     do (Ind bv,bt) <- check gam (ptovenv env) scrutinee Nothing
+>     do (bv,bt) <- check gam (ptovenv env) scrutinee Nothing
 >        let (Ind btnorm) = (normaliseEnv (ptovenv env) gam bt)
->        let bvin = makePsEnv (map fst env) bv
+>        let (Ind bvnorm) = (normaliseEnv (ptovenv env) gam bv)
+>        let bvin = makePsEnv (map fst env) bvnorm
 >        let btin = makePsEnv (map fst env) btnorm
 >        let indices = getArgs btin
 >        let ty = getFun btin
diff --git a/Ivor/Typecheck.lhs b/Ivor/Typecheck.lhs
--- a/Ivor/Typecheck.lhs
+++ b/Ivor/Typecheck.lhs
@@ -12,6 +12,8 @@
 > import Ivor.Unify
 > import Ivor.Constant
 > import Ivor.Errors
+> import Ivor.Evaluator
+> import Ivor.Values
 
 > import Control.Monad.State
 > import Data.List
@@ -93,7 +95,7 @@
 > type Level = Int
 
 > data FileContext = FC FilePath Int
->   deriving Eq
+>   deriving (Show, Eq)
 
 > errCtxt :: Maybe FileContext -> IError -> IError
 > errCtxt (Just (FC f l)) err = IContext (f ++ ":" ++ show l ++ ":") err
@@ -121,20 +123,25 @@
 >          let ty' = papp subst ty
 >          return (Ind tm',Ind ty')
 
->    where mkSubst xs = mkSubst' (P,[]) xs
->          mkSubst' acc [] = return acc
->          mkSubst' acc (q:xs) 
->             = do acc' <- mkSubstQ acc q
->                  mkSubst' acc' xs
+Handy to pass through all the variables, for tracing purposes when debugging.
+
+>    where mkSubst xs = mkSubst' (P,[]) xs xs
+>          mkSubst' acc [] all = return acc
+>          mkSubst' acc (q:xs) all
+>             = do acc' <- mkSubstQ acc q all
+>                  mkSubst' acc' xs all
 >
->          mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,fc))
+>          eqn (ok, (env, x, y, fc)) = if ok then (x,y,fc) else (x,y,Nothing)
+>          showeqn all = concat $ map ((++"\n").show.eqn) all
+
+>          mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,fc)) all
 >             = do -- (s',nms) <- mkSubst xs
 >                  let x' = papp s' x
->                  let (Ind y') = normalise gam (Ind (papp s' y))
->                  uns <- 
->                         case unifyenvErr ok gam env (Ind x') (Ind y') of
->                           Right x' -> return x'
->                           Left err -> ifail (errCtxt fc err)
+>                  let (Ind y') = eval_nf gam (Ind (papp s' y))
+>                  uns <- case unifyenvErr ok gam env (Ind y') (Ind x') of
+>                           Right uns -> {- trace (show (y', x', uns)) $ -} return uns
+>                           Left err -> {- trace (showeqn all) $ -} 
+>                                       ifail (errCtxt fc (ICantUnify (Ind y') (Ind x')))
 
                          Failure err -> fail $ err ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms
 
@@ -150,6 +157,15 @@
 >          delta n ty n' | n == n' = ty
 >                        | otherwise = P n'
 
+> convertAllEnv :: Gamma Name -> 
+>                  [(Env Name, Indexed Name, Indexed Name,Maybe FileContext)] ->
+>                  Env Name -> IvorM (Env Name)
+> convertAllEnv gam constraints [] = return []
+> convertAllEnv gam constraints ((n,B b t):xs) 
+>       = do (Ind t', _) <- doConversion RStar gam constraints (Ind t) (Ind Star)
+>            xs' <- convertAllEnv gam constraints xs
+>            return ((n,B b t'):xs')
+
 > check :: Gamma Name -> Env Name -> Raw -> Maybe (Indexed Name) -> 
 >          IvorM (Indexed Name, Indexed Name)
 > check gam env tm mty = do
@@ -175,7 +191,11 @@
 >    -- rename all the 'inferred' things to another generated name,
 >    -- so that they actually get properly checked on the rhs
 >    let realNames = mkNames next
+>    -- The environment will need the conversions applying, to fill in any implicit
+>    -- variables in the pattern
+>    e <- convertAllEnv gam bs e
 >    e' <- renameB gam realNames (renameBinders e)
+>    (v1, t1) <- doConversion tm1 gam bs v1 t1
 >    (v1', t1') <- fixupGam gam realNames (v1, t1)
 >    (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1') 
 >    -- Drop names out of e' that don't appear in v1'' as a result of the
@@ -212,7 +232,11 @@
 >    -- rename all the 'inferred' things to another generated name,
 >    -- so that they actually get properly checked on the rhs
 >    let realNames = mkNames next
+>    -- The environment will need the conversions applying, to fill in any implicit
+>    -- variables in the pattern
+>    e <- convertAllEnv gam bs e
 >    e' <- renameB gam realNames (renameBinders e)
+>    (v1, t1) <- doConversion tm1 gam bs v1 t1
 >    (v1', t1') <- fixupGam gam realNames (v1, t1)
 >    (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1') 
 >    -- Drop names out of e' that don't appear in v1'' as a result of the
@@ -292,7 +316,7 @@
 >     -- Then check the resulting type matches the expected type.
 >     if infer then (case exp of
 >              Nothing -> return ()
->              Just expty -> checkConvSt env gamma expty tmty )
+>              Just expty -> checkConvSt env gamma tmty expty )
 >       else return ()
 >     -- Then fill in any remained inferred values we got by knowing the
 >     -- expected type
@@ -330,7 +354,7 @@
 >    where mkTT (Just (i, B _ t)) _ = return (Ind (P n), Ind t)
 >          mkTT Nothing (Just ((Fun _ _),t)) = return (Ind (P n), t)
 >          mkTT Nothing (Just ((Partial _ _),t)) = return (Ind (P n), t)
->          mkTT Nothing (Just ((PatternDef _ _),t)) = return (Ind (P n), t)
+>          mkTT Nothing (Just ((PatternDef _ _ _),t)) = return (Ind (P n), t)
 >          mkTT Nothing (Just (Unreducible,t)) = return (Ind (P n), t)
 >          mkTT Nothing (Just (Undefined,t)) = return (Ind (P n), t)
 >          mkTT Nothing (Just ((ElimRule _),t)) = return (Ind (Elim n), t)
@@ -345,12 +369,14 @@
 
 >          defaultResult = do
 >              (next, infer, bindings, errs, mvs, fc) <- get
->              if infer
->                 then case exp of
+>              case lookup n bindings of
+>                Nothing -> 
+>                 if infer then case exp of
 >                        Nothing -> lift $ ifail (errCtxt fc (INoSuchVar n))
 >                        Just (Ind t) -> do put (next, infer, (n, B Pi t):bindings, errs, mvs, fc)
 >                                           return (Ind (P n), Ind t)
->                 else lift $ ifail (errCtxt fc (INoSuchVar n))
+>                          else lift $ ifail (errCtxt fc (INoSuchVar n))
+>                Just (B Pi t) -> return (Ind (P n), Ind t)
 
 >  tc env lvl (RApp f a) exp = do
 >     (Ind fv, Ind ft) <- tcfixup env lvl f Nothing
@@ -360,10 +386,10 @@
 >       case (fnfng,fnf) of
 >        ((Ind (Bind _ (B Pi s) (Sc t))),_) -> do
 >          (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s))
->          let sty = (normaliseEnv env emptyGam (Ind s))
+>          let sty = (normaliseEnv env gamma (Ind s))
 >          let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t))
 >          let tmty = (normaliseEnv env emptyGam (Ind tt))
->          checkConvSt env gamma (Ind at) (Ind s)
+>          checkConvSt env gamma (Ind at) sty
 >          return (Ind (App fv av), tmty)
 >        (_, (Ind (Bind _ (B Pi s) (Sc t)))) -> do
 >          (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s))
@@ -520,18 +546,23 @@
 >  checkbinder gamma env lvl n (B Lambda t) = do
 >     (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
 >     let ttnf = normaliseEnv env gamma (Ind tt)
+>     let (Ind tvnf) = normaliseEnv env gamma (Ind tv)
 >     case ttnf of
->       (Ind Star) -> return (B Lambda tv)
->       (Ind (P (MN ("INFER",_)))) -> return (B Lambda tv)
+>       (Ind Star) -> return (B Lambda tvnf)
+>       (Ind (P (MN ("INFER",_)))) -> return (B Lambda tvnf)
 >       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
 >  checkbinder gamma env lvl n (B Pi t) = do
 >     (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
->     let ttnf = normaliseEnv env gamma (Ind tt)
->     case ttnf of
->       (Ind Star) -> return (B Pi tv)
->       (Ind (P (MN ("INFER",_)))) -> return (B Pi tv)
->       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
+>     let (Ind tvnf) = normaliseEnv env gamma (Ind tv)
+>     -- let ttnf = normaliseEnv env gamma (Ind tt)
+>     checkConvSt env gamma (Ind tt) (Ind Star)
+>     return (B Pi tvnf)
 
+     case ttnf of
+       (Ind Star) -> return (B Pi tv)
+       (Ind (P (MN ("INFER",_)))) -> return (B Pi tv)
+       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
+
 >  checkbinder gamma env lvl n (B (Let v) RInfer) = do
 >     (Ind vv,Ind vt) <- tcfixup env lvl v Nothing
 >     return (B (Let vv) vt)
@@ -705,35 +736,6 @@
 > checkNotHoley i (Bind _ _ (Sc s)) = checkNotHoley (i+1) s
 > checkNotHoley i (Proj _ _ t) = checkNotHoley i t
 > checkNotHoley _ _ = return ()
-
-> pToV :: Eq n => n -> (TT n) -> (Scope (TT n))
-> pToV = pToV2 0
-
-> pToV2 v p (P n) | p==n = Sc (V v)
->                 | otherwise = Sc (P n)
-> pToV2 v p (V w) = Sc (V w)
-> pToV2 v p (Con t n i) = Sc (Con t n i)
-> pToV2 v p (TyCon n i) = Sc (TyCon n i)
-> pToV2 v p (Meta n t) = Sc (Meta n (getSc (pToV2 v p t)))
->				where getSc (Sc a) = a
-> pToV2 v p (Elim n) = Sc (Elim n)
-> pToV2 v p (Bind n b (Sc sc)) = Sc (Bind n (fmap (getSc.(pToV2 v p)) b)
->                                    (pToV2 (v+1) p sc))
->				where getSc (Sc a) = a
-> pToV2 v p (App f a) = Sc $ App (getSc (pToV2 v p f))
->                               (getSc (pToV2 v p a))
->				where getSc (Sc a) = a
-> pToV2 v p (Label t (Comp n ts)) = Sc $ Label (getSc (pToV2 v p t))
->                                         (Comp n (map (getSc.(pToV2 v p)) ts))
-> pToV2 v p (Call (Comp n ts) t) = Sc $ Call 
->                                        (Comp n (map (getSc.(pToV2 v p)) ts))
->                                        (getSc (pToV2 v p t))
-> pToV2 v p (Return t) = Sc $ Return (getSc (pToV2 v p t))
-> pToV2 v p (Proj n i t) = Sc $ Proj n i (getSc (pToV2 v p t))
->				where getSc (Sc a) = a
-> pToV2 v p (Stage t) = Sc $ Stage (sLift (getSc.(pToV2 v p)) t)
-> pToV2 v p (Const x) = Sc (Const x)
-> pToV2 v p Star = Sc Star
 
  checkR g t = (typecheck g t):: (Result (Indexed Name, Indexed Name)) 
 
diff --git a/Ivor/Unify.lhs b/Ivor/Unify.lhs
--- a/Ivor/Unify.lhs
+++ b/Ivor/Unify.lhs
@@ -5,6 +5,8 @@
 > import Ivor.Nobby
 > import Ivor.TTCore
 > import Ivor.Errors
+> import Ivor.Evaluator
+> import Ivor.Values
 
 > import Data.List
 
@@ -43,10 +45,17 @@
 >     case unifynferr i env (p x)
 >                           (p y) of
 >           (Right x) -> return x
->           _ -> unifynferr i env (p (normalise (gam' gam) x))
->                                 (p (normalise (gam' gam) y))
->    where p (Ind t) = Ind (makePs t)
+
+>           _ -> {- trace (dbgtt x ++ ", " ++ dbgtt y ++"\n") $ -}
+>                unifynferr i env (p (eval_nf (gam' gam) x))
+>                                 (p (eval_nf (gam' gam) y))
+
+           _ -> unifynferr i env (p (normalise (gam' gam) x))
+                                 (p (normalise (gam' gam) y))
+
+>    where p (Ind t) = Ind t --(makePs t)
 >          gam' g = concatGam g (envToGamHACK env)
+>          dbgtt (Ind x) = show x -- debugTT x
 
 Make the local environment something that Nobby knows about. Very hacky...
 
@@ -75,6 +84,15 @@
 >              | x == y = return acc
 >              | loc x envl == loc y envr && loc x envl >=0
 >                  = return acc
+>              | hole envl x && hole envl y = return ((x, (P y)): acc)
+>          un envl envr (Bind x (B Lambda ty) (Sc (App scl (P x')))) y acc
+>                | x == x' = un envl envr scl y acc
+>          un envl envr y (Bind x (B Lambda ty) (Sc (App scr (P x')))) acc
+>                | x == x' = un envl envr y scr acc
+>          un envl envr (Bind x (B Lambda ty) (Sc (App scl (V 0)))) y acc
+>                = un envl envr y scl acc
+>          un envl envr y (Bind x (B Lambda ty) (Sc (App scr (V 0)))) acc
+>                = un envl envr y scr acc
 >          un envl envr (P x) t acc | hole envl x = return ((x,t):acc)
 >          un envl envr t (P x) acc | hole envl x = return ((x,t):acc)
 >          un envl envr (Bind x b@(B Hole ty) (Sc sc)) t acc
@@ -82,6 +100,10 @@
 >          un envl envr (Bind x b (Sc sc)) (Bind x' b' (Sc sc')) acc =
 >              do acc' <- unb envl envr b b' acc
 >                 un ((x,b):envl) ((x',b'):envr) sc sc' acc'
+>          un envl envr (Bind x b@(B (Let v) ty) (Sc sc)) t acc
+>             = un ((x,b):envl) envr sc t acc
+>          un envl envr t (Bind x b@(B (Let v) ty) (Sc sc)) acc
+>             = un envl ((x,b):envr) t sc acc
 >                 -- combine bu scu
 >          -- if unifying the functions fails because the names are different,
 >          -- unifying the arguments is going to be a waste of time bec
diff --git a/Ivor/Values.lhs b/Ivor/Values.lhs
new file mode 100644
--- /dev/null
+++ b/Ivor/Values.lhs
@@ -0,0 +1,212 @@
+> {-# OPTIONS_GHC -fglasgow-exts #-}
+
+FIXME: Most of this stuff and Ivor.Nobby have GOT TO GO!!!
+
+> module Ivor.Values where
+
+> import Ivor.TTCore
+> import Ivor.Gadgets
+> import Ivor.Constant
+
+> import Debug.Trace
+> import Data.Typeable
+> import Control.Monad.State
+> import List
+> import qualified Data.Map as Map
+
+To begin, we need to define the context in which normalisation takes place.
+The context maps names to user defined functions, constructors and
+elimination rules.
+
+Global represents all possible global names --- if it's a user defined
+name, hold its definition, otherwise hold what it is so we know what
+to do with it, when the time comes.
+
+> data Global n
+>     = Fun [FunOptions] (Indexed n)    -- User defined function
+>     | Partial (Indexed n) [n] -- Unfinished definition
+>     | PatternDef (PMFun n) Bool Bool -- Pattern matching definition, totality, generated
+>     | ElimRule ElimRule  -- Elimination Rule
+>     | PrimOp PrimOp EvPrim     -- Primitive function
+>     | DCon Int Int       -- Data Constructor, tag and arity
+>     | TCon Int (Elims n) -- Type Constructor and arity, elim rule name
+>     | Unreducible        -- Unreducible name
+>     | Undefined          -- Declared but undefined name
+
+> data Elims n = Elims { elimRuleName :: n,
+>                        caseRuleName :: n,
+>                        constructors :: [n] }
+>              | NoConstructorsYet
+
+> data FunOptions = Frozen | Recursive | Total
+>   deriving Eq
+
+> instance Show n => Show (Global n) where
+>     show (Fun opts t) = "Fun " ++ show t
+>     show (ElimRule _) = "<<elim rule>>"
+>     show (PrimOp _ _) = "<<primitive operator>>"
+>     show (DCon x t) = "DCon " ++ show x ++ "," ++show t
+>     show (TCon x (Elims e c cons)) = "TCon " ++ show x
+>     show Unreducible = "Unreducible"
+>     show Undefined = "Undefined"
+
+> type Plicity = Int
+
+> defplicit :: Int
+> defplicit = 0
+
+> data Ord n => Gval n = G (Global n) (Indexed n) Plicity
+>    deriving Show
+
+> getglob (G v t p) = v
+> gettype (G v t p) = t
+> getplicity (G v t p) = p
+
+> newtype Ord n => Gamma n = Gam (Map.Map n (Gval n))
+>     deriving Show
+
+> extend (Gam x) (n,v) = Gam (Map.insert n v x)
+
+> emptyGam :: Ord n => Gamma n
+> emptyGam = Gam Map.empty
+
+> getAList :: Ord n => Gamma n -> [(n,(Gval n))]
+> getAList (Gam n) = Map.toAscList n
+
+> lookupval :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Global n)
+> lookupval n (Gam xs) = fmap getglob (Map.lookup n xs)
+
+> lookuptype :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Indexed n)
+> lookuptype n (Gam xs) = fmap gettype (Map.lookup n xs)
+
+> glookup ::  (Ord n, Eq n) => n -> Gamma n -> Maybe (Global n,Indexed n)
+> glookup n (Gam xs) = fmap (\x -> (getglob x,gettype x)) (Map.lookup n xs)
+
+Get a type name from the context
+
+> getTyName :: Monad m => Gamma Name -> Name -> m Name
+> getTyName  gam n = case lookuptype n gam of
+>                            Just (Ind ty) -> return $ getFnName ty
+>                            Nothing -> fail $ "No such name " ++ show n
+>   where getFnName (TyCon x _) = x
+>         getFnName (App f x) = getFnName f
+>         getFnName (Bind _ _ (Sc x)) = getFnName x
+>         getFnName x = MN ("Dunno: "++show x, 0)
+
+Return whether a name is a recursive constructor (i.e, its family name
+occurs anywhere in its arguments).
+
+> recCon :: Name -> Gamma Name -> Bool
+> recCon n gam = case glookup n gam of
+>                  (Just (DCon _ t, Ind ty)) ->
+>                      checkRec (conFamily ty) (map snd (getExpected ty))
+>                  _ -> False
+>    where conFamily t = fname (getFun (getReturnType t))
+>          fname (TyCon n _) = n
+>          fname _ = MN ("ERROR!",0)
+>          checkRec n [] = False
+>          checkRec n (x:xs) = nameOccurs n (forget x) || checkRec n xs
+
+> insertGam :: Ord n => n -> Gval n -> Gamma n -> Gamma n
+> insertGam nm val (Gam gam) = Gam $ Map.insert nm val gam
+
+> concatGam :: Ord n => Gamma n -> Gamma n -> Gamma n
+> concatGam (Gam x) (Gam y) = Gam (Map.union x y)
+
+> setFrozen :: (Ord n, Eq n) => n -> Bool -> Gamma n -> Gamma n
+> setFrozen n freeze (Gam xs) = Gam $ Map.mapWithKey sf xs where
+>    sf p (G (Fun opts v) ty plicit)
+>        | n == p = (G (Fun (doFreeze freeze opts) v) ty plicit)
+>    sf _ x = x
+>    doFreeze True opts = nub (Frozen:opts)
+>    doFreeze False opts = opts \\ [Frozen]
+
+> setRec :: (Ord n, Eq n) => n -> Bool -> Gamma n -> Gamma n
+> setRec n frec (Gam xs) = Gam $ Map.mapWithKey sf xs where
+>    sf p (G (Fun opts v) ty plicit)
+>        | n == p = (G (Fun (doFrec frec opts) v) ty plicit)
+>    sf _ x = x
+>    doFrec True opts = nub (Recursive:opts)
+>    doFrec False opts = opts \\ [Recursive]
+
+
+> freeze :: (Ord n, Eq n) => n -> Gamma n -> Gamma n
+> freeze n gam = setFrozen n True gam
+
+> thaw :: (Ord n, Eq n) => n -> Gamma n -> Gamma n
+> thaw n gam = setFrozen n False gam
+
+Remove a name from the middle of the context - should only be valid
+if it's a partial definition or an axiom which is about to be replaced.
+
+> remove :: (Ord n, Eq n) => n -> Gamma n -> Gamma n
+> remove n (Gam xs) = Gam $ Map.delete n xs
+
+Insert a name into the context. If the name is already there, this
+is an error *unless* the old definition was 'Undefined', in which case
+the name is replaced.
+
+> gInsert :: (Monad m, Ord n, Eq n, Show n) => 
+>            n -> Gval n -> Gamma n -> m (Gamma n)
+> gInsert nm val (Gam xs) = case Map.lookup nm xs of
+>         -- FIXME: Check ty against val
+>       Nothing -> return $ Gam (Map.insert nm val xs)
+>       Just (G Undefined ty _) -> return $ Gam (Map.insert nm val xs)
+>       Just (G (TCon _ NoConstructorsYet) ty _) -> 
+>                                  return $ Gam (Map.insert nm val xs)
+>       Just _ -> fail $ "Name " ++ show nm ++ " is already defined"
+
+
+An ElimRule is a Haskell implementation of the iota reductions of
+a family.
+
+> type ElimRule = Spine Value -> Maybe Value
+
+A PrimOp is an external operation
+
+> type PrimOp = Spine Value -> Maybe Value
+> type EvPrim = [TT Name] -> Maybe (TT Name) -- same, but with tt terms rather than values
+
+
+Model represents normal forms, including Ready (reducible) and Blocked
+(non-reducible) forms.
+
+> data Model s = MR (Ready s)
+>              | MB (Blocked s, Model s) (Spine (Model s))
+
+> data Ready s
+>     = RdBind Name (Binder (Model s)) (s (Model s))
+>     | RCon Int Name (Spine (Model s))
+>     | RTyCon Name (Spine (Model s))
+>     | forall c. Constant c => RdConst c
+>     | RdStar
+>     | RdLabel (Model s) (MComp s)
+>     | RdCall (MComp s) (Model s)
+>     | RdReturn (Model s)
+>     | RdCode (Model s)
+>     | RdQuote (Model s) -- (TT Name)
+>     | RdInfer
+
+> data Blocked s
+>     = BCon Int Name Int
+>     | BTyCon Name Int
+>     | BElim ElimRule Name
+>     | BPatDef (PMFun Name) Name
+>     | BPrimOp PrimOp Name
+>     | BRec Name Value
+>     | BP Name
+>     | BV Int
+>     | BEval (Model s) (Model s)
+>     | BEscape (Model s) (Model s)
+
+> data MComp s = MComp Name [Model s]
+
+> newtype Weakening = Wk Int
+
+Second weakening is cached to prevent function composition in the weaken
+class.
+
+> newtype Kripke x = Kr (Weakening -> x -> x, Weakening)
+
+> type Value = Model Kripke
+> type Normal = Model Scope
diff --git a/Ivor/ViewTerm.lhs b/Ivor/ViewTerm.lhs
--- a/Ivor/ViewTerm.lhs
+++ b/Ivor/ViewTerm.lhs
@@ -18,7 +18,7 @@
 >                        Term(..), ViewTerm(..), Annot(..), apply,
 >                        view, viewType, ViewConst, typeof, 
 >                        freeIn, namesIn, occursIn, subst, getApp, 
->                        Ivor.ViewTerm.getFnArgs,
+>                        Ivor.ViewTerm.getFnArgs, transform,
 >                        getArgTypes, Ivor.ViewTerm.getReturnType,
 >                        dbgshow,
 >                        -- * Inductive types
@@ -32,6 +32,9 @@
 
 > import Data.Typeable
 > import Data.List
+> import Data.Binary
+> import Control.Monad
+> import Debug.Trace
 
 > name :: String -> Name
 > name = UN
@@ -51,7 +54,7 @@
 > -- is for. 
 > data NameType = Bound | Free | DataCon | TypeCon | ElimOp 
 >               | Unknown -- ^ Use for sending to typechecker.
->   deriving Show
+>   deriving (Show, Enum)
 
 > -- | Construct a term representing a variable
 > mkVar :: String -- ^ Variable name
@@ -81,6 +84,8 @@
 
 > data Annot = FileLoc FilePath Int -- ^ source file, line number
 
+
+
 > instance Eq ViewTerm where
 >     (==) (Name _ x) (Name _ y) = x == y
 >     (==) (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') = f == f' && a == a'
@@ -102,6 +107,8 @@
 >     (==) (Ivor.ViewTerm.Eval t) (Ivor.ViewTerm.Eval t') = t==t'
 >     (==) (Ivor.ViewTerm.Escape t) (Ivor.ViewTerm.Escape t') = t==t'
 >     (==) (Annotation _ t) (Annotation _ t') = t == t'
+>     (==) (Annotation _ t) t' = t == t'
+>     (==) t (Annotation _ t') = t == t'
 >     (==) _ _ = False
 
 > -- | Haskell types which can be used as constants
@@ -203,6 +210,7 @@
 >         = Ivor.ViewTerm.Eval (vtaux ctxt tm)
 >     vtaux ctxt (Stage (TTCore.Escape tm _)) 
 >         = Ivor.ViewTerm.Escape (vtaux ctxt tm)
+>     vtaux ctxt (Meta n _) = Metavar n
 >     vtaux _ t = error $ "Can't happen vtaux " ++ debugTT t
 
 > -- | Return whether the name occurs free in the term.
@@ -295,15 +303,17 @@
 > -- | Match the second argument against the first, returning a list of
 > -- the names in the first paired with their matches in the second. Returns
 > -- Nothing if there is a match failure. There is no searching under binders.
-> match :: ViewTerm -> ViewTerm -> Maybe [(Name, ViewTerm)]
-> match t1 t2 = do acc <- m' t1 t2 []
->                  checkDups acc [] where
->   m' (Name _ n) t acc = return ((n,t):acc)
+> matchMeta :: ViewTerm -> ViewTerm -> Maybe [(Name, ViewTerm)]
+> matchMeta t1 t2 = do acc <- m' t1 t2 []
+>                      checkDups acc [] where
+>   m' (Metavar n) t acc = return ((n,t):acc)
+>   m' Placeholder t acc = return acc
 >   m' (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') acc 
 >       = do acc' <- m' f f' acc
 >            m' a a' acc'
 >   m' (Annotation _ t) t' acc = m' t t' acc
 >   m' t (Annotation _ t') acc = m' t t' acc
+>   m' (Name _ x) (Name _ y) acc | x == y = return acc
 >   m' x y acc | x == y = return acc
 >              | otherwise = fail $"Mismatch " ++ show x ++ " and " ++ show y
 
@@ -314,6 +324,16 @@
 >                                else fail $ "Mismatch on " ++ show x
 >          Nothing -> checkDups xs ((x,t):acc)
 
+> replaceMeta :: [(Name, ViewTerm)] -> ViewTerm -> ViewTerm
+> replaceMeta ms (Metavar n) = case lookup n ms of
+>                                Just t -> t
+>                                _ -> Metavar n
+> replaceMeta ms (Ivor.ViewTerm.App f a)
+>             = Ivor.ViewTerm.App (replaceMeta ms f) (replaceMeta ms a)
+> replaceMeta ms (Annotation a t) = Annotation a (replaceMeta ms t)
+> replaceMeta ms x = x
+
+
 > -- |Substitute a name n with a value v in a term f 
 > subst :: Name -> ViewTerm -> ViewTerm -> ViewTerm
 > subst n v nm@(Name _ p) | p == n = v
@@ -346,3 +366,43 @@
 > subst n v (Annotation a t) = Annotation a (subst n v t)
 > subst n v t = t
 
+> -- |Transform a term according to a rewrite rule.
+> transform :: ViewTerm -- ^ Left hand side, with metavariables
+>           -> ViewTerm -- ^ Right hand side, with metavariables
+>           -> ViewTerm -- ^ Term to rewrite
+>           -> ViewTerm
+> transform lhs rhs term = tr' term where
+>     tr' (Ivor.ViewTerm.App f a) 
+>             = doTr $ Ivor.ViewTerm.App (tr' f) (tr' a)
+>     tr' (Ivor.ViewTerm.Lambda v t sc) 
+>             = doTr $ Ivor.ViewTerm.Lambda v (tr' t) (tr' sc)
+>     tr' (Ivor.ViewTerm.Forall v t sc) 
+>             = doTr $ Ivor.ViewTerm.Forall v (tr' t) (tr' sc)
+>     tr' (Ivor.ViewTerm.Let v t val sc) 
+>             = doTr $ Ivor.ViewTerm.Let v (tr' t) (tr' val) (tr' sc)
+>     tr' (Annotation a t) = doTr $ Annotation a (tr' t)
+>     tr' x = doTr x
+
+>     doTr x = case matchMeta lhs x of
+>                 Just vars -> replaceMeta vars rhs
+>                 Nothing -> x
+
+> instance Binary Name where
+>     put (UN s) = do put (0 :: Word8); put s
+>     put (MN s) = do put (1 :: Word8); put s
+
+>     get = do tag <- getWord8
+>              case tag of
+>                0 -> liftM UN get
+>                1 -> liftM MN get
+
+> instance Binary NameType where
+>     put x = put (fromEnum x)
+>     get = do t <- get
+>              return (toEnum t)
+
+> instance Binary Annot where
+>     put (FileLoc p i) = do put p; put i
+>     get = do p <- get
+>              i <- get
+>              return (FileLoc p i)
diff --git a/ivor.cabal b/ivor.cabal
--- a/ivor.cabal
+++ b/ivor.cabal
@@ -1,5 +1,5 @@
 Name:		ivor
-Version:	0.1.9
+Version:	0.1.10
 Author:		Edwin Brady
 License:	BSD3
 License-file:	LICENSE
@@ -58,7 +58,7 @@
 
 
 
-Build-depends:  base >=3 && <5, parsec, mtl, directory
+Build-depends:  base >=3 && <5, parsec, mtl, directory, binary
 Build-type:     Simple
 
 Extensions:     MultiParamTypeClasses, FunctionalDependencies,
@@ -72,7 +72,7 @@
 		Ivor.Plugin, Ivor.Construction
 Other-modules:	Ivor.Nobby, Ivor.TTCore, Ivor.State,
 		Ivor.Tactics, Ivor.Typecheck, Ivor.Evaluator
-		Ivor.Gadgets, Ivor.SC, Ivor.Bytecode,
+		Ivor.Gadgets, Ivor.SC, Ivor.Bytecode, Ivor.Values,
 		Ivor.CodegenC, Ivor.Datatype, Ivor.Display,
 		Ivor.ICompile, Ivor.MakeData, Ivor.Unify,
 		Ivor.Grouper, Ivor.ShellParser, Ivor.Constant,