Skip to content

Instantly share code, notes, and snippets.


Robin Green greenrd

View GitHub Profile
greenrd / gist:1b2824aae85b1c4219b3
Created May 4, 2015
Set existential quantification working
View gist:1b2824aae85b1c4219b3
trait Id[E]
class C[TC[_[_]]] {
val d: Set[Id[I] forSome { type I }] = ???
d.contains((???): Id[TC[Id]])
View emacsd-tile.el
;; emacsd-tile.el -- tiling windows for emacs
;; Sep 2010: Modified by Robin Green <> to use modified cursor keys
(defun swap-with (dir)
(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))
View gist:334380
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.
View gist:334374
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)
View gist:275550
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
View gist:275487
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 '' 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", "", "gnome-doc-make-C.omf"])
sydbox@1263322520: Reason: connect{family=AF_INET addr= po
View gist:273088
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
View gist:273073
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'
!{ in void test::TestCase::call_run(): Test threw unexpected exception paludis::PtyError (message grantpt(3) failed: Exec format error, backtrace When creating pty FDs: -> )
(repeat): pt_chown: needs to be installed setuid `root'