|
|
|
|
|
|
by dunham
974 days ago
|
|
|
Not sure if it's what you're asking for, but in lean, you can put `sorry` to skip a proof. It's `believe_me` in Idris2, and I think the Agda version is `trustMe`. You can also use stuff like ! when you don't want to prove your array indices (it might crash or substitute a dummy value if you're wrong). |
|
|