Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
View Tickets
Search
Context Navigation
Back to Ticket #375
Ticket #375
: pg_bug3.v
File pg_bug3.v,
131 bytes
(added by
megacz
,
14 years ago
)
Line
1
Require Import Coq
.
Init
.
Logic
.
2
3
4
Notation
"C 'áµáŽŸ'"
:=
(
fun x
=>
C
)
(
at level
20
).
5
6
Definition crash_the_rooster f
:=
f
áµáŽŸ
.
Download in other formats:
Original Format