@@ -1701,6 +1701,9 @@ runTactical fc env tm = do tm' <- eval tm
17011701 new_tyDecls e }
17021702 aux <- getAux
17031703 returnUnit
1704+ | n == tacN "prim__DefineFunction", [decl] <- args
1705+ = do undefined
1706+ undefined
17041707 | n == tacN "prim__Debug", [ty, msg] <- args
17051708 = do let msg' = fromTTMaybe msg
17061709 case msg' of
@@ -2879,6 +2882,22 @@ reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)
28792882 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
28802883reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
28812884
2885+reifyFunDefn :: Term -> ElabD RFunDefn
2886+reifyFunDefn (App (App (P _ n _) fnN) clauses)
2887+ | n == tacN "DefineFun" =
2888+ do fnN' <- reifyTTName fnN
2889+ clauses' <- case unList clauses of
2890+ Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
2891+ Just cs -> mapM reifyC cs
2892+ return $ RDefineFun fnN' clauses'
2893+ where reifyC :: Term -> ElabD RFunClause
2894+ reifyC (App (App (P (DCon _ _ _) n _) lhs) rhs)
2895+ | n == tacN "MkFunClause" = liftM2 RMkFunClause
2896+ (reifyRaw lhs)
2897+ (reifyRaw rhs)
2898+ reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
2899+reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
2900+
28822901envTupleType :: Raw
28832902envTupleType
28842903 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")