search

JetBrains / arend-lib

Apache License 2.0
79 stars 23 forks source link

Make composition operator o infix #61

Open s3midetnov opened 7 months ago

s3midetnov commented 7 months ago

in src/Category.ard instead of | \fixl 8 o \alias \infixl 8 ∘ {X Y Z : Ob} : Hom Y Z -> Hom X Y -> Hom X Z make | \infixl 8 o \alias \infixl 8 ∘ {X Y Z : Ob} : Hom Y Z -> Hom X Y -> Hom X Z