aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 9 Pull Requests 3 Packages Projects Releases 1 Wiki Activity

fix: Option setting in REPL #71

Merged
aniva merged 1 commits from lib/mkOptions into dev 2024-04-15 12:58:08 -07:00
Conversation 0 Commits 1 Files Changed 2 +1 -17
2 changed files with 1 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Pantograph.lean
View File

@ -81,6 +81,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty, printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
printExprPretty := args.printExprPretty?.getD options.printExprPretty, printExprPretty := args.printExprPretty?.getD options.printExprPretty,
printExprAST := args.printExprAST?.getD options.printExprAST, printExprAST := args.printExprAST?.getD options.printExprAST,
printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars,
noRepeat := args.noRepeat?.getD options.noRepeat, noRepeat := args.noRepeat?.getD options.noRepeat,
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls, printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps

17
Pantograph/Library.lean
View File

@ -82,23 +82,6 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
def envCatalog: Lean.CoreM Protocol.EnvCatalogResult := def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
Environment.catalog ({}: Protocol.EnvCatalog) Environment.catalog ({}: Protocol.EnvCatalog)
@[export pantograph_mk_options]
def mkOptions
(printJsonPretty: Bool)
(printExprPretty: Bool)
(printExprAST: Bool)
(noRepeat: Bool)
(printAuxDecls: Bool)
(printImplementationDetailHyps: Bool)
: Protocol.Options := {
printJsonPretty,
printExprPretty,
printExprAST,
noRepeat,
printAuxDecls,
printImplementationDetailHyps,
}
@[export pantograph_env_inspect_m] @[export pantograph_env_inspect_m]
def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options): def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) := Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=