Robin Green greenrd
greenrd
/ gist:1b2824aae85b1c4219b3
Created
May 4, 2015 19:20
Set existential quantification working
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
| trait Id[E] | |
| class C[TC[_[_]]] { | |
| val d: Set[Id[I] forSome { type I }] = ??? | |
| d.contains((???): Id[TC[Id]]) | |
| } |
greenrd
/ emacsd-tile.el
Created
September 8, 2010 15:01
— forked from mariusae/emacsd-tile.el
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
| ;; emacsd-tile.el -- tiling windows for emacs | |
| ;; Sep 2010: Modified by Robin Green <[email protected]> to use modified cursor keys | |
| (defun swap-with (dir) | |
| (interactive) | |
| (let ((other-window (windmove-find-other-window dir))) | |
| (when other-window | |
| (let* ((this-window (selected-window)) | |
| (this-buffer (window-buffer this-window)) | |
| (other-buffer (window-buffer other-window)) |
greenrd
/ gist:334380
Created
March 16, 2010 19:13
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
| Inductive TupleT : nat -> Type := | |
| nilT : TupleT 0 | |
| | consT {n} A : (A -> TupleT n) -> TupleT (S n). | |
| Require Import Relations. | |
| Inductive TupleT_direct_subterm : relation (sigT TupleT) := | |
| TupleT_sub n A (x : A) F : TupleT_direct_subterm (existT _ n (F x)) (existT _ _ (consT A F)). | |
| Require Import Subterm. |
greenrd
/ gist:334374
Created
March 16, 2010 19:10
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
| Error: | |
| In environment | |
| n : nat | |
| A : TupleT n | |
| B : TupleT n | |
| tm2 : TupleMap n A B | |
| The term | |
| "(fun (P : forall (n : nat) (T U : TupleT n), TupleMap n T U -> Type) | |
| (z : P 0 nilT nilT tmNil) | |
| (s : forall (n : nat) (A B : Type) (F : A -> TupleT n) |
greenrd
/ gist:275550
Created
January 12, 2010 20:06
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
| greenrd@cspcnh ~ $ man inquisitio | |
| Error executing formatting or display command. | |
| System command (cd "/usr/share/man" && (echo ".ll 15.8i"; echo ".nr LL 15.8i"; echo ".pl 1100i"; /bin/cat '/usr/share/man/man1/inquisitio.1'; echo ".\\\""; echo ".pl \n(nlu+10") | /usr/bin/gtbl | /usr/bin/nroff -mandoc -c | /usr/bin/less) exited with status 256. | |
| No manual entry for inquisitio |
greenrd
/ gist:275487
Created
January 12, 2010 19:03
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
| make[1]: Entering directory `/var/tmp/paludis/build/gnome-desktop-gnome-doc-utils-0.17.3/work/gnome-doc-utils-0.17.3/doc' | |
| Making check in gnome-doc-make | |
| make[2]: Entering directory `/var/tmp/paludis/build/gnome-desktop-gnome-doc-utils-0.17.3/work/gnome-doc-utils-0.17.3/doc/gnome-doc-make' | |
| xmllint --noout --noent --path C:./C --xinclude --postvalid ./C/gnome-doc-make.xml | |
| xmllint --noout --xinclude --dtdvalid 'http://scrollkeeper.sourceforge.net/dtds/scrollkeeper-omf-1.0/scrollkeeper-omf.dtd' gnome-doc-make-C.omf | |
| sydbox@1263322520: Access Violation! | |
| sydbox@1263322520: Child Process ID: 12397 | |
| sydbox@1263322520: Child CWD: /var/tmp/paludis/build/gnome-desktop-gnome-doc-utils-0.17.3/work/gnome-doc-utils-0.17.3/doc/gnome-doc-make | |
| sydbox@1263322520: Last Exec: execve("/usr/bin/xmllint", ["xmllint", "--noout", "--xinclude", "--dtdvalid", "http://scrollkeeper.sourceforge.net/dtds/scrollkeeper-omf-1.0/scrollkeeper-omf.dtd", "gnome-doc-make-C.omf"]) | |
| sydbox@1263322520: Reason: connect{family=AF_INET addr=192.168.122.1 po |
greenrd
/ gist:273088
Created
January 9, 2010 20:32
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
| root@cspcnh util # ls -ld /dev /dev/ptmx /dev/pts | |
| drwxrwxrwt 3 root root 200 2010-01-09 13:11 /dev | |
| lrwxrwxrwx 1 root root 13 2010-01-09 13:11 /dev/ptmx -> /dev/pts/ptmx | |
| drwxr-xr-x 2 root root 0 2010-01-09 13:11 /dev/pts | |
| root@cspcnh util # ls -ld /dev/pts/ptmx | |
| crw-rw-rw- 1 root root 5, 2 2010-01-09 20:31 /dev/pts/ptmx |
greenrd
/ gist:273073
Created
January 9, 2010 20:16
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
| FAIL: pty_TEST (exit: 255) | |
| ========================== | |
| Test program /var/tmp/paludis/build/sys-apps-paludis-scm/work/paludis-scm/paludis/util/.libs/pty_TEST: | |
| * "ptys": pt_chown: needs to be installed setuid `root' | |
| !{ | |
| test_framework.cc:193: in void test::TestCase::call_run(): Test threw unexpected exception paludis::PtyError (message grantpt(3) failed: Exec format error, backtrace When creating pty FDs: -> ) | |
| } NOT OK | |
| (repeat): pt_chown: needs to be installed setuid `root' | |
| !{ |