SkySkimmer

After    | File Name                                                                                        | Before   || Change   
-----------------------------------------------------------------------------------------------------------------------------------
3m20.88s | Total                                                                                            | 3m17.92s || +0m02.96s
-----------------------------------------------------------------------------------------------------------------------------------
0m18.30s | [notation-overridden,parsing]
theories/Spaces/BAut/Bool                                          | 0m18.39s || -0m00.08s
0m12.34s | [notation-overridden,parsing]
theories/Algebra/ooGroup                                           | 0m11.77s || +0m00.57s
0m07.99s | [notation-overridden,parsing]
theories/Modalities/ReflectiveSubuniverse                          | 0m07.75s || +0m00.24s

SkySkimmer

(defun help-what-about ()
  "Returns nil if called in non help-mode derived buffer.
Otherwise guesses what the help buffer is about.
If it succeeds the guess is returned as a string. Otherwise returns nil.

Heuristics:
If the buffer starts with a known symbol (i.e. in `obarray') that's our result.
This may return the wrong thing: imagine a mode where `t t' runs `foo', we will
think `describe-key' is talking about `t' alone.
If someone defines `Enabled' we will be similarly confused after `describe-mode', etc."

SkySkimmer

Set Universe Polymorphism.
Set Printing Universes. Set Printing All.
Unset Strict Universe Declaration.

(**
A vector is a list of size n whose elements belong to a set A. *)

Inductive t A : nat -> Type :=
  |nil : t A 0
  |cons : forall (h:A) (n:nat), t A n -> t A (S n).

SkySkimmer

Notation idmap := (fun x => x).

Notation compose := (fun g f x => g (f x)).

Notation "g 'o' f" := (compose g f) (at level 40, left associativity).

Record Equiv A B := BuildEquiv {
  equiv_fun : A -> B ;
  equiv_inv : B -> A

SkySkimmer

Require Import Utf8.
Require Import Setoid.
Require Import ChoiceFacts.

Definition ext := ∀ A B, ∀ R : A -> A -> Prop, ∀ T : A -> B -> Prop, Equivalence R ->
  (∀ x x' y, R x x' -> T x y -> T x' y) ->
  (∀ x, ∃ y, T x y) ->
  ∃ f : A -> B, ∀ x : A, T x (f x) /\ (∀ x' : A, R x x' -> f x = f x').

Definition alt := forall A (R : A -> A -> Prop),

SkySkimmer

as
at
Axiom
by
cofix
CoFixpoint
CoInductive
Definition
discriminated
else

SkySkimmer

Debug:
Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded
Debug:
1: looking for (E
                  (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id
                   ∘ id ∘ id ∘ id ∘ f0 ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id)) without backtracking
Debug: 1.1: simple apply d_is_e with pattern (E ?META1205) on
(E
   (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id
    ∘ f0 ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id)), 1 subgoal(s)

SkySkimmer

After    | File Name                                                 | Before   || Change   
--------------------------------------------------------------------------------------------
5m00.32s | Total                                                     | 5m33.52s || -0m33.20s
--------------------------------------------------------------------------------------------
0m42.07s | Spaces/BAut/Bool                                          | 0m50.32s || -0m08.25s
0m21.63s | Categories/Category/Sigma/Univalent                       | 0m24.02s || -0m02.39s
0m11.69s | Algebra/ooGroup                                           | 0m14.13s || -0m02.44s
0m08.02s | Spaces/Finite                                             | 0m10.33s || -0m02.31s
0m08.02s | Spaces/BAut/Rigid                                         | 0m09.30s || -0m01.28s
0m07.28s | Spaces/BAut                                               | 0m09.05s || -0m01.77s

SkySkimmer

File "checker/closure.ml", line 320, characters 2-83:
File "checker/closure.ml", line 326, characters 2-100:
File "checker/closure.ml", line 331, characters 26-176:
File "checker/closure.ml", line 341, characters 2-446:
File "checker/closure.ml", line 364, characters 28-358:
File "checker/closure.ml", line 389, characters 2-233:
File "checker/closure.ml", line 511, characters 4-503:
File "checker/closure.ml", line 562, characters 35-366:
File "checker/closure.ml", line 576, characters 31-667:
File "checker/closure.ml", line 599, characters 2-670:

SkySkimmer

Require Import Classical.

Class Neg (P:Prop) :=
  { neg : Prop;
    neg_ok : ~ P -> neg }.

Arguments neg P {_}.
Arguments neg_ok P {_} _.

Lemma neg_right (A B:Prop) `{!Neg A} : (neg A -> B) -> A \/ B.