Leanサンプル funcomp

section funcomp
  variables {X Y Z:Type}
  def comp (f:X → Y) (g:Y → Z) :X → Z :=
    λ x:X, g (f x)
end funcomp

#check comp
infix `;` := comp

constants A B C D:Type
constants (f:A → B) (g:B → C) (h:C → D)
#check comp 
#check comp f  g
#check f;g;h
#check  f ; @id B