blob: 28b40f32d920b4cfdac837ba6ad2fa060d6ee6e0 [file] [edit]
1
0
"ho!\n"
"hu!\n"
100001
100000
0
0
0
"<stdin>:1:0: warning: using 'exit' to interrupt Lean\n"
none
some 0