Macro System

Stream: new members

[Simon Daniel]

Hello,
lets image a Inductive I that wraps a value of a. UnwrapType is the Type of a function that unwraps the value of a. I now want to express a computation on values of I a based on an unwrapping function so i can access their values. concrete instances of my compType now have to declare a named lambda expression and whenever i want to do computations on my "I a" values i have to call this named lambda first.
this happens alot so i want a nicer way, i thought of automatically introducing a named lambda with name "un" and allways appliing this "un" function when a "I a" Value appears.
maybe someone can help me or point to some helpful resources, i guess the metaprogramming book could help but it seems somewhat scary to me

inductive I (a:Type) where
| some: a -> I a

def unwrap  : I a -> a
| .some v => v

def UnwrapType  := {a:Type} ->  I a -> a

def v1: I Nat := .some 2
def v2: I String := .some "two"
--....
def compType := UnwrapType -> Unit

def calc1: compType :=
  fun un =>
    let concat := toString  (un v1) ++ (un v2)
    ()
--... lots of calcs

[Damiano Testa]

I am not sure that I understand what you are after, but is this good for you?

inductive I (a:Type) where
| some: a -> I a

def unwrap  : I a -> a
| .some v => v

--  instruct Lean how to print `I`s
instance {a} [ToString a] : ToString (I a) where
  toString x := "I " ++ toString (unwrap x)

def v1: I Nat := .some 2
def v2: I String := .some "two"

#eval v1 -- I 2
#eval v2 -- I two

[Simon Daniel]

that is not what i was going for
i want to express computations (Values of "compType") that depend on an concrete interpretation of an "I a". so UnwrapType is the type of any function that can unwrap/interpret an "I.a".

def compType (a:Type) := UnwrapType -> a

compType is also meant to produce meaningful values, not just Unit.
also suppose unwrap is not the only function of type UnwrapType
the string concatenation served as an example for using "I a" values in a computation

my problem is when defining computations

 def x: compType Nat :=
  fun un =>
     (un v1) + (un v2).length

there is alot of boilerplate code. i dont care for the function name being "un", and whenever i use a "I a" value in the following part i want to apply this "un" function, so i want to be able to write something like this

def x: compType Nat  :=
     v1 + v2.length

i hope this clarifies my intend :sweat_smile: