search

kosmikus / lhs2tex

Preprocessor for typesetting Haskell sources with LaTeX
Other
99 stars 28 forks source link

Agda infix comma operator is rendered incorrectly #19

Open asr opened 12 years ago

asr commented 12 years ago

Given the data type

data _∧_ (A B : Set) : Set where
  _,_ : A → B → A ∧ B

the following function

foo : ∀ {A B} → A → B → A ∧ B
foo a b = a , b

is rendered incorrectly because the spaces before and after the comma are removed.