I'm using the Lean computer proof assistant and customizing some notation. Here's the example I'm working with:
def comp (X Y Z : Type*) (g : [Y, Z]) (f : [X, Y]) (x : X) : Z := g (f x)
constant X : Type
constant Y : Type
constant Z : Type
constant f : X \rightarrow Y
constant g : Y \rightarrow Z
def h := comp(X)(Y)(Z)(g)(f)
One thing that would be really convenient is being able to omit characters. In the code above, it would be nice if Lean could infer the (X)(Y)(Z) in comp(X)(Y)(Z)(g)(f).
So I was hoping that somehow it would be possible for Lean to infer X and Y and Z from g and f. Is this possible?
More generally, I am interested in any notation feature in lean which could infer types of things so as to make the notation cleaner for myself.
For instance, how do I obtain the type of something for use in further computations. That is, suppose a : A, A : Type. I want to obtain A from a and construct from it the type A \rightarrow A in a closed form involving a.