dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

better name for metas
Some checks failed
Publish Playground / build (push) Has been cancelled
Details
Publish Playground / deploy (push) Has been cancelled
Details

Browse Source
This commit is contained in:
Steve Dunham
2026-02-11 13:32:45 -08:00
parent eb9921212c
commit 6a16dc6150
1 changed files with 4 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
src/Lib/Elab.newt
View File

@@ -363,6 +363,8 @@ lams Z _ tm = tm
lams (S k) Nil tm = Lam emptyFC "arg_\{show k}" Explicit Many (lams k Nil tm) lams (S k) Nil tm = Lam emptyFC "arg_\{show k}" Explicit Many (lams k Nil tm)
lams (S k) (x :: xs) tm = Lam emptyFC x Explicit Many (lams k xs tm) lams (S k) (x :: xs) tm = Lam emptyFC x Explicit Many (lams k xs tm)
unify : Env -> UnifyMode -> Val -> Val -> M UnifyResult unify : Env -> UnifyMode -> Val -> Val -> M UnifyResult
.boundNames : Context -> List String .boundNames : Context -> List String
@@ -626,7 +628,7 @@ freshMeta ctx fc ty kind = do
debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})" debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
-- need the ns here -- need the ns here
-- we were fudging this for v1 -- we were fudging this for v1
let qn = QN top.ns "\{show mc.next}" let qn = QN top.ns "$m\{show mc.next}"
let newmeta = Unsolved fc qn ctx ty kind Nil let newmeta = Unsolved fc qn ctx ty kind Nil
let autos = case kind of let autos = case kind of
AutoSolve => qn :: mc.autos AutoSolve => qn :: mc.autos
@@ -1525,6 +1527,7 @@ check ctx tm ty = do
(tm,ty) => do (tm,ty) => do
(tm', ty') <- infer ctx tm (tm', ty') <- infer ctx tm
-- REVIEW - should we look at `tm` to know how many to insert? Is there a case where this helps?
(tm', ty') <- insert ctx tm' ty' (tm', ty') <- insert ctx tm' ty'
let names = map fst ctx.types let names = map fst ctx.types