mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-15 14:23:32 +03:00
vars can be erased in evalLocal
A small thing, but no need to do that check since we can get it from locs.
This commit is contained in:
parent
a75887ffa6
commit
4a0970731e
@ -168,7 +168,7 @@ parameters (defs : Defs, topopts : EvalOpts)
|
||||
applyToStack nf _ = pure nf
|
||||
|
||||
evalLocal : {auto c : Ref Ctxt Defs} ->
|
||||
{free, vars : _} ->
|
||||
{free : _} ->
|
||||
Env Term free ->
|
||||
FC -> Maybe Bool ->
|
||||
(idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) ->
|
||||
@ -177,7 +177,7 @@ parameters (defs : Defs, topopts : EvalOpts)
|
||||
Core (NF free)
|
||||
-- If it's one of the free variables, we are done unless the free
|
||||
-- variable maps to a let-binding
|
||||
evalLocal {vars = []} env fc mrig idx prf stk locs
|
||||
evalLocal env fc mrig idx prf stk []
|
||||
= if not (holesOnly topopts || argHolesOnly topopts)
|
||||
-- if we know it's not a let, no point in even running `getBinder`
|
||||
&& fromMaybe True mrig
|
||||
|
Loading…
Reference in New Issue
Block a user