Gaëtan Gilbert SkySkimmer
SkySkimmer
/ Wrong Every Time insert images
Created
August 28, 2014 18:33
This file contains 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 WrongEveryTime image insert | |
| // @description Add image after clicked link on wrongeverytime.com | |
| // @author SkySkimmer | |
| // @version 1.1 | |
| // @history 1.1 Insert images button | |
| // @history 1.0 Initial functionality | |
| // @license GPL version 3 | |
| // @namespace SkySkimmer |
SkySkimmer
/ script.user.js
Created
August 28, 2014 18:37
This file contains 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 WrongEveryTime image insert | |
| // @description Add image after clicked link on wrongeverytime.com | |
| // @author SkySkimmer | |
| // @version 1.1 | |
| // @history 1.1 Insert images button | |
| // @history 1.0 Initial functionality | |
| // @license WTFPL | |
| // @namespace SkySkimmer |
SkySkimmer
/ Universe.v
Created
June 11, 2016 21:29
This file contains 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
| Section Univ. | |
| Universe i. | |
| Definition identity (A : Type@{i}) (x : A) := x. | |
| End Univ. | |
| Definition id2 := identity _ identity. |
SkySkimmer
/ time-of-build-both.log
Created
June 27, 2016 15:27
This file contains 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
| After | File Name | Before || Change | |
| -------------------------------------------------------------------------------------------- | |
| 3m54.98s | Total | 3m56.11s || -0m01.12s | |
| -------------------------------------------------------------------------------------------- | |
| 0m22.22s | Spaces/BAut/Bool | 0m17.15s || +0m05.07s | |
| 0m11.69s | hit/V | 0m17.53s || -0m05.84s | |
| 0m03.85s | contrib/HoTTBook | 0m05.35s || -0m01.49s | |
| 0m03.66s | Spaces/BAut/Bool/IncoherentIdempotent | 0m01.95s || +0m01.71s | |
| 0m15.91s | categories/Category/Sigma/Univalent | 0m15.39s || +0m00.51s | |
| 0m11.73s | Algebra/ooGroup | 0m11.72s || +0m00.00s |
SkySkimmer
/ bug_failed_defined_01.v
Created
June 27, 2016 15:50
This file contains 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
| (* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "theories" "HoTT" "-top" "HoTTBookExercises") -*- *) | |
| (* File reduced by coq-bug-finder from original input, then from 1168 lines to 33 lines, then from 138 lines to 34 lines, then from 220 lines to 35 lines, then from 93 lines to 37 lines, then from 118 lines to 41 lines, then from 293 lines to 52 lines, then from 350 lines to 86 lines, then from 126 lines to 85 lines, then from 296 lines to 119 lines *) | |
| (* coqc version 8.5pl1 (June 2016) compiled on Jun 27 2016 15:21:22 with OCaml 4.02.3 | |
| coqtop version 8.5pl1 (June 2016) *) | |
| Axiom proof_admitted : False. | |
| Tactic Notation "admit" := abstract case proof_admitted. | |
| Require HoTT.Basics.Equivalences. | |
| Module Export Trunc. | |
| Import HoTT.Basics.Overture. | |
| Import HoTT.Basics.Equivalences. |
SkySkimmer
/ time-of-build-both.log
Created
June 28, 2016 09:22
This file contains 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
| After | File Name | Before || Change | |
| -------------------------------------------------------------------------------------------- | |
| 3m53.94s | Total | 3m50.51s || +0m03.42s | |
| -------------------------------------------------------------------------------------------- | |
| 0m24.70s | Spaces/BAut/Bool | 0m17.13s || +0m07.57s | |
| 0m11.56s | hit/V | 0m16.72s || -0m05.15s | |
| 0m06.01s | Spaces/BAut/Bool/IncoherentIdempotent | 0m01.90s || +0m04.10s | |
| 0m15.10s | categories/Category/Sigma/Univalent | 0m15.41s || -0m00.31s | |
| 0m11.27s | Algebra/ooGroup | 0m11.32s || -0m00.05s | |
| 0m08.29s | Modalities/ReflectiveSubuniverse | 0m08.22s || +0m00.06s |
SkySkimmer
/ time-of-build-both.log
Created
June 30, 2016 14:29
This file contains 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
| After | File Name | Before || Change | |
| -------------------------------------------------------------------------------------------- | |
| 3m54.23s | Total | 3m48.72s || +0m05.51s | |
| -------------------------------------------------------------------------------------------- | |
| 0m25.18s | Spaces/BAut/Bool | 0m21.49s || +0m03.69s | |
| 0m06.02s | Spaces/BAut/Bool/IncoherentIdempotent | 0m03.96s || +0m02.05s | |
| 0m12.16s | hit/V | 0m10.88s || +0m01.27s | |
| 0m15.22s | categories/Category/Sigma/Univalent | 0m16.09s || -0m00.86s | |
| 0m11.49s | Algebra/ooGroup | 0m11.32s || +0m00.16s | |
| 0m08.13s | Modalities/ReflectiveSubuniverse | 0m08.82s || -0m00.68s |
SkySkimmer
/ time-of-build-both.log
Created
July 5, 2016 09:45
This file contains 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
| After | File Name | Before || Change | |
| -------------------------------------------------------------------------------------------- | |
| 3m45.99s | Total | 3m44.33s || +0m01.66s | |
| -------------------------------------------------------------------------------------------- | |
| 0m21.56s | Spaces/BAut/Bool | 0m21.45s || +0m00.10s | |
| 0m15.30s | categories/Category/Sigma/Univalent | 0m15.05s || +0m00.25s | |
| 0m11.54s | Algebra/ooGroup | 0m11.38s || +0m00.15s | |
| 0m10.83s | hit/V | 0m10.82s || +0m00.00s | |
| 0m08.22s | Modalities/ReflectiveSubuniverse | 0m08.11s || +0m00.11s | |
| 0m06.86s | Spaces/BAut | 0m06.47s || +0m00.39s |
SkySkimmer
/ time-of-build-both.log
Created
July 11, 2016 11:26
This file contains 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
| After | File Name | Before || Change | |
| -------------------------------------------------------------------------------------------- | |
| 3m50.23s | Total | 3m54.70s || -0m04.46s | |
| -------------------------------------------------------------------------------------------- | |
| 0m22.54s | Spaces/BAut/Bool | 0m24.20s || -0m01.66s | |
| 0m15.47s | categories/Category/Sigma/Univalent | 0m15.90s || -0m00.42s | |
| 0m11.42s | Algebra/ooGroup | 0m11.44s || -0m00.01s | |
| 0m10.91s | hit/V | 0m11.28s || -0m00.36s | |
| 0m08.18s | Modalities/ReflectiveSubuniverse | 0m08.20s || -0m00.01s | |
| 0m06.83s | contrib/Freudenthal | 0m06.72s || +0m00.11s |
SkySkimmer
/ time-of-build-both.log
Created
July 11, 2016 11:41
This file contains 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
| After | File Name | Before || Change | |
| -------------------------------------------------------------------------------------------- | |
| 3m53.88s | Total | 3m50.92s || +0m02.95s | |
| -------------------------------------------------------------------------------------------- | |
| 0m22.82s | Spaces/BAut/Bool | 0m22.60s || +0m00.21s | |
| 0m16.03s | categories/Category/Sigma/Univalent | 0m15.49s || +0m00.54s | |
| 0m11.64s | hit/V | 0m10.97s || +0m00.67s | |
| 0m11.50s | Algebra/ooGroup | 0m11.53s || -0m00.02s | |
| 0m08.18s | Modalities/ReflectiveSubuniverse | 0m08.29s || -0m00.10s | |
| 0m06.85s | categories/Adjoint/Pointwise | 0m06.82s || +0m00.02s |
OlderNewer