This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // ==UserScript== | |
| // @name Djinni Quick Apply Pro | |
| // @namespace http://tampermonkey.net/ | |
| // @version 2.2.0 | |
| // @description Automate job applications on Djinni.co directly via Tampermonkey | |
| // @author You | |
| // @match https://djinni.co/* | |
| // @grant none | |
| // ==/UserScript== |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ✘ ~/projects/mm0 learn ±✚ ./examples/test_pub_theorem.sh | |
| === Setting up test files === | |
| === First Verification (Base case) === | |
| elab test_thm.mm1 | |
| elabbed test_thm.mm1 | |
| 1 sorts, 1 term/def, 3 ax/thm | |
| Verification succeeded! | |
| === Experiment 1: Adding a new PUB theorem not declared in MM0 === | |
| elab test_thm.mm1 | |
| elabbed test_thm.mm1 |
OlderNewer