diff --git a/Justfile b/Justfile
--- a/Justfile
+++ b/Justfile
@@ -63,7 +63,7 @@
     cd polyglot && atsfmt src/concurrency.dats -i
     cd polyglot && atsfmt src/shared.dats -i
     cd polyglot && atsfmt src/filetype.sats -i
-    cd polyglot && ./shake.hs
+    cd polyglot && ./bash/setup.sh && ./build
     @rm -rf polyglot
 
 size:
diff --git a/ats-format.cabal b/ats-format.cabal
--- a/ats-format.cabal
+++ b/ats-format.cabal
@@ -1,5 +1,5 @@
 name:                ats-format
-version:             0.1.3.6
+version:             0.2.0.0
 synopsis:            A source-code formatter for ATS
 description:         An opinionated source-code formatter for [ATS](http://www.ats-lang.org/).
 homepage:            https://hub.darcs.net/vmchale/ats-format#readme
diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs
--- a/src/Language/ATS.hs
+++ b/src/Language/ATS.hs
@@ -1,10 +1,12 @@
 -- | Main module for the library
-module Language.ATS ( -- * Functions
+module Language.ATS ( -- * Functions for working with syntax
                       lexATS
                     , parseATS
                     , printATS
                     , printATSCustom
                     , printATSFast
+                    -- * Library functions
+                    , getDependencies
                     -- * Syntax Tree
                     , ATS (..)
                     , Declaration (..)
@@ -36,6 +38,7 @@
                     -- * Lenses
                     , leaves
                     , constructorUniversals
+                    -- * Library functions
                     -- * Executable
                     , exec
                     ) where
@@ -45,3 +48,10 @@
 import           Language.ATS.Parser
 import           Language.ATS.PrettyPrint
 import           Language.ATS.Types
+import Data.Maybe (catMaybes)
+
+getDependencies :: ATS -> [FilePath]
+getDependencies (ATS ds) = catMaybes (g <$> ds)
+    where g (Staload _ s) = Just s
+          g (Include s) = Just s
+          g _ = Nothing
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -430,12 +430,12 @@
           | dollar {% Left $ Expected $1 "$" "Termination metric" }
 
 -- | Parse an existential quantier on a type
-Existential : lsqbracket Args vbar Expression rsqbracket { Existential $2 False Nothing (Just $4) }
+Existential : lsqbracket Args vbar StaticExpression rsqbracket { Existential $2 False Nothing (Just $4) }
             | lsqbracket Args rsqbracket { Existential $2 False Nothing Nothing }
             | openExistential Args rsqbracket { Existential $2 True Nothing Nothing }
-            | openExistential Args vbar Expression rsqbracket { Existential $2 True Nothing (Just $4) }
+            | openExistential Args vbar StaticExpression rsqbracket { Existential $2 True Nothing (Just $4) }
             | lsqbracket Args colon Type rsqbracket { Existential $2 False (Just $4) Nothing } -- FIXME arguments should include more than just ':'
-            | lsqbracket Expression rsqbracket { Existential [] False Nothing (Just $2) }
+            | lsqbracket StaticExpression rsqbracket { Existential [] False Nothing (Just $2) }
             
 -- | Parse a universal quantifier on a type
 Universal : lbrace Args rbrace { Universal $2 Nothing Nothing }
@@ -548,13 +548,16 @@
 Signature : signature { $1 }
           | colon { "" }
 
+OptType : Type { Just $1 }
+        | { Nothing }
+
 -- | Parse a type signature and optional function body
-PreFunction : FunName openParen FullArgs closeParen Signature Type OptExpression { (PreF $1 $5 [] [] $3 $6 Nothing $7) }
-            | FunName Universals OptTermetric Signature Type OptExpression { PreF $1 $4 [] $2 [NoArgs] $5 $3 $6 }
-            | FunName Universals OptTermetric doubleParens Signature Type OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 }
-            | FunName Universals OptTermetric openParen FullArgs closeParen Signature Type OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 }
-            | Universals FunName Universals OptTermetric openParen FullArgs closeParen Signature Type OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 }
-            | Universals FunName Universals OptTermetric Signature Type OptExpression { PreF $2 $5 $1 $3 [] $6 $4 $7 }
+PreFunction : FunName openParen FullArgs closeParen Signature OptType OptExpression { (PreF $1 $5 [] [] $3 $6 Nothing $7) }
+            | FunName Universals OptTermetric Signature OptType OptExpression { PreF $1 $4 [] $2 [NoArgs] $5 $3 $6 }
+            | FunName Universals OptTermetric doubleParens Signature OptType OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 }
+            | FunName Universals OptTermetric openParen FullArgs closeParen Signature OptType OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 }
+            | Universals FunName Universals OptTermetric openParen FullArgs closeParen Signature OptType OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 }
+            | Universals FunName Universals OptTermetric Signature OptType OptExpression { PreF $2 $5 $1 $3 [] $6 $4 $7 }
             | prval {% Left $ Expected $1 "Function signature" "prval" }
             | var {% Left $ Expected $1 "Function signature" "var" }
             | val {% Left $ Expected (token_posn $1) "Function signature" "val" }
@@ -629,6 +632,8 @@
           | Operators Operator { $2 : $1 }
           | Operators identifier { to_string $2 : $1 }
 
+StackFunction : openParen Args closeParen Signature Type plainArrow Expression { StackF $4 $2 $5 $7 }
+
 -- | Parse a declaration
 Declaration : include string { Include $2 }
             | define { Define $1 }
@@ -646,8 +651,8 @@
             | val Pattern eq Expression { Val (get_addendum $1) Nothing $2 $4 }
             | var Pattern eq Expression { Var Nothing $2 (Just $4) Nothing }
             | var Pattern colon Type { Var (Just $4) $2 Nothing Nothing }
-            | var Pattern eq fixAt IdentifierOr openParen Args closeParen Signature Type plainArrow Expression { Var Nothing $2 (Just $ FixAt (PreF (Unqualified $5) $9 [] [] $7 $10 Nothing (Just $12))) Nothing }
-            | var Pattern eq lambdaAt openParen Args closeParen Signature Type plainArrow Expression { Var Nothing $2 (Just $ LambdaAt (PreF (Unnamed $4) $8 [] [] $6 $9 Nothing (Just $11))) Nothing }
+            | var Pattern eq fixAt IdentifierOr openParen Args closeParen Signature Type plainArrow Expression { Var Nothing $2 (Just $ FixAt $5 undefined) Nothing }
+            | var Pattern eq lambdaAt openParen Args closeParen Signature Type plainArrow Expression { Var Nothing $2 (Just $ LambdaAt (undefined)) Nothing }
             | prval Pattern eq Expression { PrVal $2 $4 }
             | praxi PreFunction { Func $1 (Praxi $2) }
             | primplmnt Implementation { ProofImpl $2 }
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -206,14 +206,12 @@
         a (BeginF _ e)
             | not (startsParens e) = linebreak <> indent 2 ("begin" <$> indent 2 e <$> "end")
             | otherwise = e
-        a (FixAtF (PreF n s [] [] as t Nothing (Just e))) = "fix@" <+> pretty n <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)
-        a (LambdaAtF (PreF Unnamed{} s [] [] as t Nothing (Just e))) = "lam@" <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)
+        a (FixAtF n (StackF s as t e)) = "fix@" <+> text n <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)
+        a (LambdaAtF (StackF s as t e)) = "lam@" <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)
         a (AddrAtF _ e)                = "addr@" <> e
         a (ViewAtF _ e)                = "view@" <> e
         a (ListLiteralF _ s t es)      = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es
         a BinListF{} = undefined
-        a FixAtF{} = undefined
-        a LambdaAtF{} = undefined
         a CallF{} = undefined
         prettyCases []              = mempty
         prettyCases [(s, l, t)]     = "|" <+> pretty s <+> pretty l <+> t
@@ -242,7 +240,8 @@
         a (ExistentialPatternF e p)    = pretty e <> p
 
 singleArg :: Arg -> Doc
-singleArg = argHelper (<>)
+singleArg x@Arg{} = argHelper (<>) x
+singleArg x       = pretty x
 
 argHelper :: (Doc -> Doc -> Doc) -> Arg -> Doc
 argHelper _ (Arg (First s))   = pretty s
@@ -322,6 +321,7 @@
 
 instance Pretty Existential where
     pretty (Existential [] b Nothing (Just e)) = withHashtag b <+> pretty e <+> rbracket
+    pretty (Existential [x@Arg{}] b Nothing Nothing) = withHashtag b <> singleArg x <> rbracket
     pretty (Existential bs b ty Nothing)  = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbracket
     pretty (Existential bs b ty (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbracket
         where go (Arg (First s))  = pretty s
@@ -476,20 +476,20 @@
 -- FIXME figure out a nicer algorithm for when/how to split lines.
 -- aka don't use '</>' in places.
 instance Pretty PreFunction where
-    pretty (PreF i si [] [] [NoArgs] rt Nothing (Just e)) = pretty i <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack
-    pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si [] [] as rt (Just t) (Just e)) = pretty i </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si [] us as rt (Just t) (Just e)) = pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si [] us [NoArgs] rt Nothing (Just e)) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si [] us as rt Nothing (Just e)) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si pus [] as rt (Just t) (Just e)) = fancyU pus </> pretty i <+> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si pus us as rt (Just t) (Just e)) = fancyU pus </> pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si pus us as rt Nothing (Just e)) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt
-    pretty (PreF i si [] us [] rt Nothing Nothing) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt
-    pretty (PreF i si [] us as rt Nothing Nothing) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt
-    pretty (PreF i si pus us as rt Nothing Nothing) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt
+    pretty (PreF i si [] [] [NoArgs] (Just rt) Nothing (Just e)) = pretty i <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack
+    pretty (PreF i si [] [] as (Just rt) Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] [] as (Just rt) (Just t) (Just e)) = pretty i </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] us as (Just rt) (Just t) (Just e)) = pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] us [NoArgs] (Just rt) Nothing (Just e)) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] us as (Just rt) Nothing (Just e)) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si pus [] as (Just rt) Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si pus [] as (Just rt) (Just t) (Just e)) = fancyU pus </> pretty i <+> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si pus us as (Just rt) (Just t) (Just e)) = fancyU pus </> pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si pus us as (Just rt) Nothing (Just e)) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] [] as (Just rt) Nothing Nothing) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt
+    pretty (PreF i si [] us [] (Just rt) Nothing Nothing) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt
+    pretty (PreF i si [] us as (Just rt) Nothing Nothing) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt
+    pretty (PreF i si pus us as (Just rt) Nothing Nothing) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt
     pretty _ = undefined
 
 instance Pretty DataPropLeaf where
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -37,6 +37,7 @@
     , StaticExpression (..)
     , StaticExpressionF (..)
     , Fixity (..)
+    , StackFunction (..)
     , rewriteATS
     , rewriteDecl
     -- * Lenses
@@ -191,7 +192,7 @@
     deriving (Show, Eq, Generic, NFData)
 
 -- | Wrapper for existential quantifiers/types
-data Existential = Existential { boundE :: [Arg], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe Expression }
+data Existential = Existential { boundE :: [Arg], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe StaticExpression }
     deriving (Show, Eq, Generic, NFData)
 
 -- | @~@ is used to negate numbers in ATS
@@ -277,8 +278,8 @@
                 | Begin AlexPosn Expression
                 | BinList { _op :: BinOp, _exprs :: [Expression] }
                 | PrecedeList { _exprs :: [Expression] }
-                | FixAt PreFunction
-                | LambdaAt PreFunction
+                | FixAt String StackFunction
+                | LambdaAt StackFunction
                 | ParenExpr AlexPosn Expression
                 deriving (Show, Eq, Generic, NFData)
 
@@ -304,12 +305,19 @@
               | CastFn PreFunction
               deriving (Show, Eq, Generic, NFData)
 
+data StackFunction = StackF { stSig        :: String
+                            , stArgs       :: [Arg]
+                            , stReturnType :: Type
+                            , stExpression :: Expression
+                            }
+                            deriving (Show, Eq, Generic, NFData)
+
 data PreFunction = PreF { fname         :: Name -- ^ Function name
                         , sig           :: String -- ^ e.g. <> or \<!wrt>
                         , preUniversals :: [Universal] -- ^ Universal quantifiers making a function generic
                         , universals    :: [Universal] -- ^ Universal quantifiers/refinement type
                         , args          :: [Arg] -- ^ Actual function arguments
-                        , returnType    :: Type -- ^ Return type
+                        , returnType    :: Maybe Type -- ^ Return type
                         , termetric     :: Maybe StaticExpression -- ^ Optional termination metric
                         , expression    :: Maybe Expression -- ^ Expression holding the actual function body (not present in static templates)
                         }
diff --git a/test/data/concurrency.out b/test/data/concurrency.out
--- a/test/data/concurrency.out
+++ b/test/data/concurrency.out
@@ -12,29 +12,28 @@
 absvtype queue_vtype(a : vt@ype+, int) = ptr
 
 vtypedef queue(a : vt0p, id : int) = queue_vtype(a, id)
-vtypedef queue(a : vt0p) = [ id : int ] queue(a, id)
+vtypedef queue(a : vt0p) = [id:int] queue(a, id)
 
 absprop ISNIL (id : int, b : bool)
 
 extern
 fun {a:vt0p} queue_is_nil {id:int} (!queue(a, id)) :
-  [ b : bool ] (ISNIL(id, b) | bool(b))
+  [b:bool] (ISNIL(id, b) | bool(b))
 
 absprop ISFULL (id : int, b : bool)
 
 extern
 fun {a:vt0p} queue_is_full {id:int} (!queue(a, id)) :
-  [ b : bool ] (ISFULL(id, b) | bool(b))
+  [b:bool] (ISFULL(id, b) | bool(b))
 
 extern
 fun {a:vt0p} queue_insert {id:int}
 (ISFULL(id,false) | xs : !queue(a, id) >> queue(a, id2), x : a) :
-  #[ id2 : int ] void
+  #[id2:int] void
 
 extern
 fun {a:vt0p} queue_remove {id:int}
-(ISNIL(id,false) | xs : !queue(a, id) >> queue(a, id2)) :
-  #[ id2 : int ] a
+(ISNIL(id,false) | xs : !queue(a, id) >> queue(a, id2)) : #[id2:int] a
 
 extern
 fun {a:vt0p} queue_make  (cap : intGt(0)) : queue(a)
@@ -172,12 +171,12 @@
 implement {a} channel_make (cap) =
   let
     extern
-    praxi __assert() : [ l : agz ] void
+    praxi __assert() : [l:agz] void
     
-    prval [ l0 : addr ]() = __assert()
-    prval [ l1 : addr ]() = __assert()
-    prval [ l2 : addr ]() = __assert()
-    prval [ l3 : addr ]() = __assert()
+    prval [l0:addr]() = __assert()
+    prval [l1:addr]() = __assert()
+    prval [l2:addr]() = __assert()
+    prval [l3:addr]() = __assert()
     val chan = CHANNEL{l0,l1,l2,l3}(_)
     val+ CHANNEL (ch) = chan
     val () = ch.cap := cap
diff --git a/test/data/fast-combinatorics.out b/test/data/fast-combinatorics.out
--- a/test/data/fast-combinatorics.out
+++ b/test/data/fast-combinatorics.out
@@ -31,7 +31,7 @@
   end
 
 // FIXME
-fun bad(n : int) : [ m : nat ] int(m) =
+fun bad(n : int) : [m:nat] int(m) =
   case+ n of
     | 0 => 0
     | n => 1 + bad(n - 1)
@@ -43,7 +43,7 @@
       begin
         let
           var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))
-          var bound: [ m : nat ] int(m) = bad(pre_bound)
+          var bound: [m:nat] int(m) = bad(pre_bound)
           
           fun loop {n:nat}{m:nat} .<max(0,m-n)>. (i : int(n), bound : int(m)) :<>
             bool =
diff --git a/test/data/filetype.out b/test/data/filetype.out
--- a/test/data/filetype.out
+++ b/test/data/filetype.out
@@ -5,8 +5,8 @@
 typedef command_line = @{ version = bool
                         , help = bool
                         , table = bool
-                        , excludes = [ m : nat ] list(string, m)
-                        , includes = [ m : nat ] list(string, m)
+                        , excludes = [m:nat] list(string, m)
+                        , includes = [m:nat] list(string, m)
                         }
 
 // Program state, tracking *all* supported file types in an unboxed structure.
diff --git a/test/data/left-pad.out b/test/data/left-pad.out
--- a/test/data/left-pad.out
+++ b/test/data/left-pad.out
@@ -8,7 +8,7 @@
 fun left_pad { p, l : nat | p > 0 && l > 0 } ( pad : ssize_t(p)
                                              , c : charNZ
                                              , s : strnptr(l)
-                                             ) : [ cushion : nat ] (PAD(p, l, cushion) | strnptr(cushion+l))
+                                             ) : [cushion:nat] (PAD(p, l, cushion) | strnptr(cushion+l))
 
 extern
 fun {t:t@ype} fill_list {n:nat} (size : ssize_t(n), c : t) :
@@ -51,7 +51,7 @@
     val _ = if list_vt_length(args) = 3 then
       (let
         val c = '0'
-        val s = g1ofg0(args[1]) : [ n : nat ] string(n)
+        val s = g1ofg0(args[1]) : [n:nat] string(n)
         val pad = g1ofg0(g0string2int(args[2]))
       in
         if length(s) > 0 && pad > 0 then
diff --git a/test/data/number-theory.out b/test/data/number-theory.out
--- a/test/data/number-theory.out
+++ b/test/data/number-theory.out
@@ -9,8 +9,8 @@
 
 // Existential types for even and odd numbers. These are only usable with the
 // ATS library.
-typedef Even = [ n : nat ] int(2*n)
-typedef Odd = [ n : nat ] int(2*n+1)
+typedef Even = [n:nat] int(2*n)
+typedef Odd = [n:nat] int(2*n+1)
 
 // TODO jacobi symbol
 // fn legendre(a: int, p: int) : int =
diff --git a/test/data/numerics.out b/test/data/numerics.out
--- a/test/data/numerics.out
+++ b/test/data/numerics.out
@@ -24,13 +24,13 @@
           1
       end
 
-castfn lemma_bounded(i : int) : [ n : nat ] int(n) =
+castfn lemma_bounded(i : int) : [n:nat] int(n) =
   $UN.cast(i)
 
-fun sqrt_bad(k : intGt(0)) : [ m : nat ] int(m) =
+fun sqrt_bad(k : intGt(0)) : [m:nat] int(m) =
   let
     var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))
-    var bound: [ m : nat ] int(m) = lemma_bounded(pre_bound)
+    var bound: [m:nat] int(m) = lemma_bounded(pre_bound)
   in
     bound
   end