inductive foo : Type := | bar : foo | baz : foo と書きたくなるが、:= は要らない。なぜなのだろう？[追記]match/with/end の省略と同じみたいだ。[/追記]

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 …