Minor changes

This commit is contained in:
2026-01-31 12:52:01 -08:00
parent f3a18fa658
commit eed5c09508
4 changed files with 14 additions and 4 deletions

View File

@@ -669,8 +669,6 @@ primType fc nm = do
Just (MkEntry _ name ty (PrimTCon _) _) => pure $ VRef fc name Lin
_ => error fc "Primitive type \{show nm} not in scope"
infer : Context -> Raw -> M (Tm × Val)
data Bind = MkBind String Icit Val
instance Show Bind where
@@ -1431,6 +1429,7 @@ updateRec ctx fc clauses arg ty = do
getTele Nothing v = error (getFC v) "Expected a pi type, got \{show v}"
getTele _ v = error (getFC v) "Expected a record type, got \{show v}"
infer : Context -> Raw -> M (Tm × Val)
check ctx tm ty = do
ty' <- forceType ctx.env ty

View File

@@ -716,6 +716,13 @@ instance Functor IO where
uncurry : a b c. (a b c) (a × b) c
uncurry f (a,b) = f a b
curry : a b c. (a × b c) (a b c)
curry f a b = f (a,b)
-- TODO Belongs in prelude, but I need to rename a function in Lib.Compile (or let local win over imports)
-- apply : ∀ a b. (a → b) → a → b
-- apply f a = f a
-- TODO Idris has a tail recursive version of this
instance Applicative List where
return a = a :: Nil