User defined option

Stream: lean4

[Horatiu Cheval]

I'm struggling with the following basic example where I'm trying to define my own option an set it.

import Lean.Data.Options

open Lean

register_option my_option : Bool := {defValue := true, descr := "This is my option"}

set_option my_option false
/-
unknown option 'my_option'
-/

I guess I'm misunderstanding something fundamental here. Could anyone help me out?

[Alexander Bentkamp]

You need to create a second file and import the file containing register_option from there. Only then the option will really become available.

[Horatiu Cheval]

Great, thanks!

[Horatiu Cheval]

One further trouble here. Basically what I'm trying to do is to define a conditional unexpander that depends on the value of an option. So

inductive Term
| var : Nat → Term

open Term

notation "Variable" => var

@[appUnexpander var]
def unexpandVar : Lean.PrettyPrinter.Unexpander
| `(var $i) => `($i)
| _ => throw ()


@[appUnexpander var]
def unexpandVar' : Lean.PrettyPrinter.Unexpander
| `(var $i) => `(Variable $i)
| _ => throw ()

def t := var 7

set_option show_v true

#reduce t
/-
Should print
Variable 7
-/
set_option show_v false

#reduce t
/-
Should print 7
-/

I want to join the two unexpanders into a single definition that checks the value of the show_v option and then decides what to do.
I tried calling Lean.getBoolOption show_v.name (after wrapping the definition in do block) but that doesn't work with

failed to synthesize instance
  Lean.MonadOptions Lean.PrettyPrinter.UnexpandM

What's the right way to do this?

[Jannis Limperg]

Can't be done afaict: UnexpandM = EStateM Unit Unit, so you don't have access to options in this monad. You can try to define a delaborator instead, that should run in a monad that has access to options.