snu-sf / paco

A Coq library for parametric coinduction
https://github.com/snu-sf/paco
Other
43 stars 10 forks source link

Notation 추가 #7

Closed alxest closed 3 years ago

alxest commented 6 years ago

아래 Notation 들을 정의해서 쓰고 있는데 paconotation 에 넣는건 어떨까요?

top2 = (fun _ _ => True)
~2 p = (fun x0 x1 => ~ (p x0 x1))
p /2\ q = (fun x0 x1 => p x0 x1 /\ q x0 x1)
jeehoonkang commented 6 years ago

@alxest This is now a public repo, so I think it'd be better to report bugs in English. Thanks!