@@ -153,13 +153,18 @@ elab ist info pattern opts fn tm
153153
154154 local f = do e <- get_env
155155 return (f `elem` map fst e)
156−
156+
157+ -- | Is a constant a type?
158+ constType :: Const -> Bool
157159 constType (AType _) = True
158160 constType StrType = True
159161 constType PtrType = True
160162 constType VoidType = True
161163 constType _ = False
162164
165+ elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
166+ -> PTerm -- ^ The term to elaborate
167+ -> ElabD ()
163168 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
164169 elab' ina PType = do apply RType []; solve
165170 elab' (_,_,inty) (PConstant c)
@@ -607,6 +612,14 @@ elab ist info pattern opts fn tm
607612 mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!
608613 addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])
609614
615+ -- | Elaborate the arguments to a function
616+ elabArgs :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
617+ -> [Bool]
618+ -> FC -- ^ Source location
619+ -> Bool
620+ -> [Name] -- ^ Names of arguments - these identify the holes to be filled
621+ -> [(Bool, PTerm)] -- ^ (Laziness, argument)
622+ -> ElabD ()
610623 elabArgs ina failed fc retry [] _
611624-- | retry = let (ns, ts) = unzip (reverse failed) in
612625-- elabArgs ina [] False ns ts