| # You can append the following functions to your `.profile` file | |
| function venv_help() { | |
| echo "venv list ....... list environments" | |
| echo "venv del myenv .. delete 'myenv'" | |
| echo "venv off ........ deactivate the current environment" | |
| echo "venv myenv ...... create 'myenv' if it doesn't exist then activate it;" | |
| echo " just activate it otherwise" | |
| } |
This is a personal attempt to pierce through the hard walls of ZK constructions. I don't want to skip any detail that would obscure my own understanding. Hopefully this is enough to have the same effect on the reader.
Disclaimer
Elegance are succintness is non-goals. If there is a slower argument, mechanical even, I will choose it.
| axiom two_plus_two_is_five: 2 + 2 = 5 | |
| theorem i_can_prove_false: False := by | |
| have two_plus_two_is_four: 2 + 2 = 4 := by simp | |
| have contradiction := Eq.trans two_plus_two_is_five.symm two_plus_two_is_four | |
| exact absurd contradiction (by simp) | |
| theorem i_can_prove_anything_1: 5 - 2 = 2 := by | |
| have: False → 5 - 2 = 2 := by simp | |
| exact this i_can_prove_false |