7 lines · 216 B · Text
RawDownload
1/1: Building WithLift (WithLift.idr)Main> succNotZero : S k = 0 -> VoidsuccNotZeroMain> recNotEqLift : (k = j -> Void) -> S k = S j -> Void(recNotEqLift contra)Main> recNotEq f Refl = f ReflMain> Bye for now!

Keyboard shortcuts

General

Show keyboard shortcuts
?
Focus the current search
/

Issues and pull requests

Open filters
f

Issues, pull requests and Inbox

Select next item
j↓
Select previous item
k↑
Open selected item
Enter
Dismiss filters or clear selection
Esc

Repository code

Go to file
t