chore: Version 0.3 #136
|
@ -68,7 +68,8 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
|
||||||
match e with
|
match e with
|
||||||
| .fvar fvarId =>
|
| .fvar fvarId =>
|
||||||
let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
|
let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
|
||||||
assert! (← getLCtx).contains fvarId'
|
-- Delegating this to `Meta.check` later
|
||||||
|
--assert! (← getLCtx).contains fvarId'
|
||||||
return .done $ .fvar fvarId'
|
return .done $ .fvar fvarId'
|
||||||
| .mvar mvarId => do
|
| .mvar mvarId => do
|
||||||
-- Must not be assigned
|
-- Must not be assigned
|
||||||
|
|
Loading…
Reference in New Issue