mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-13 07:26:59 +03:00
2d503f1c8a
safeForget broke things due to missing case. Also added a test to ensure it doesn't happen again.
7 lines
38 B
Plaintext
7 lines
38 B
Plaintext
:p arhs
|
|
intro x
|
|
intros
|
|
trivial
|
|
qed
|
|
:q
|