Skip to content

Commit

Permalink
fix for missing constants when translating module
Browse files Browse the repository at this point in the history
  • Loading branch information
rish987 committed Mar 21, 2024
1 parent caacd0b commit 0c065c7
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion Main.lean
Expand Up @@ -64,7 +64,9 @@ def runTransCmd (p : Parsed) : IO UInt32 := do
onlyConstsArr := _onlyConsts.map (·.toName)
else
printColor BLUE s!">> Using all constants from given module: {moduleName}..."
onlyConstsArr := ⟨env.constants.map₂.toList.map fun (x : Name × Lean.ConstantInfo) => x.1
let some moduleIdx := Lean.Environment.getModuleIdx? env moduleName | throw $ IO.userError s!"main module {moduleName} not found"
let moduleConstNames := env.header.moduleData.get! moduleIdx |>.constNames.toList
onlyConstsArr := ⟨moduleConstNames⟩

let onlyConstsInit := onlyConstsArr.foldl (init := default) fun acc const =>
if !const.isImplementationDetail && !const.isCStage then acc.insert const else acc
Expand Down

0 comments on commit 0c065c7

Please sign in to comment.