Skip to content

Instantly share code, notes, and snippets.

View vlj's full-sized avatar

vlj

33 followers · 5 following
View GitHub Profile
@vlj
vlj / gist:db1f93e50652e7244f72f37ba467646b
Created June 8, 2020 17:39
checking whether to enable maintainer-specific portions of Makefiles... yes
checking for a BSD-compatible install... /usr/bin/install -c
checking whether build environment is sane... yes
checking for a thread-safe mkdir -p... /bin/mkdir -p
checking for gawk... gawk
checking whether make sets $(MAKE)... yes
checking whether make supports nested variables... yes
checking whether ln -s works... yes
checking whether make sets $(MAKE)... (cached) yes
configure: Will look for Coq executables only in /mnt/c/Users/vljno/Source/Repos/HoTT/coq-HoTT/bin
@vlj
vlj / gist:738767900150266de4169a2895c00c83
Created June 8, 2020 17:36
checking whether to enable maintainer-specific portions of Makefiles... yes
checking for a BSD-compatible install... /usr/bin/install -c
checking whether build environment is sane... yes
checking for a thread-safe mkdir -p... /bin/mkdir -p
checking for gawk... gawk
checking whether make sets $(MAKE)... yes
checking whether make supports nested variables... yes
checking whether ln -s works... yes
checking whether make sets $(MAKE)... (cached) yes
checking for coqtop... /home/vlj/.opam/default/bin/coqtop
@vlj
vlj / order.v
Created April 27, 2020 21:56
From mathcomp Require Import classical_sets eqtype boolp seq order topology choice ssrfun.
Require Import ssreflect ssrbool.
Open Scope classical_set_scope.
Module SetOrder.
Section SetOrder.
Context {T: Type}.
@vlj
vlj / ring3.v
Created April 1, 2020 18:20
From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.
Import GRing.Theory.
Variable R: numFieldType.
Open Scope ring_scope.
@vlj
vlj / ring2.v
Last active April 4, 2020 01:23
From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.
Open Scope ring_scope.
Import GRing.Theory.
Variable R: numFieldType.
Definition rt :
@vlj
vlj / ring.v
Created March 30, 2020 18:19
From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.
Open Scope ring_scope.
Import GRing.Theory.
Variable R: numFieldType.
Lemma tmp:
@vlj
vlj / order.v
Created February 19, 2020 20:05
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice path.
From mathcomp Require Import div fintype tuple finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg ssrnum.
From mathcomp Require Import ssrint matrix order ssrint order.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
@vlj
vlj / le_refl.v
Created February 17, 2020 20:33
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice path.
From mathcomp Require Import div fintype tuple finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg ssrnum.
From mathcomp Require Import ssrint matrix order ssrint order.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
@vlj
vlj / leP.v
Created February 16, 2020 12:39
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice path.
From mathcomp Require Import div fintype tuple finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg ssrnum falgebra.
From mathcomp Require Import ssrint matrix algC order.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
@vlj
vlj / omega.v
Created February 15, 2020 19:55
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice path.
From mathcomp Require Import div fintype tuple finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg ssrnum falgebra.
From mathcomp Require Import ssrint matrix algC.
Require Omega.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.