Yasu Watanabe
Results
3
comments of
Yasu Watanabe
I created a branch based on this issue. https://github.com/ywata/plfa.github.io/tree/pr-06 I also created a repository of unicode instruction generator in https://github.com/ywata/plfa_tool/unicode_instruction
In Equality section of Equality chapter: `_≡_` is defined like this ``` data _≡_ {A : Set} (x : A) : A → Set where refl : x ≡ x...
Oh. Sorry to bother you but I'm really waiting for your update!