Skip to content

Instantly share code, notes, and snippets.

open import Data.Nat
open import Data.Fin
module StrictlyPositive where
-- The following datatype is accepted by Agda, but rejected
-- by Coq
data Ty : Set0 -> Set0 where
c1 : Ty ℕ
c2 : Ty (Ty ℕ)
@csgordon
csgordon / fsharp-debian.md
Last active February 28, 2017 09:18
Setting up F# on Debian

Installing F# on Debian

In theory you should be able to install the mono-devel package from Debian, then grab the latest checkout of F#'s Github repository and build. Unfortunately, the most recent versions of Debian's (and Ubuntu's) mono-devel package (3.0.6) include a lovely bug that breaks the F# build (https://bugzilla.xamarin.com/show_bug.cgi?id=10884). Another alternative is installing Debian Sid (unstable branch), where there are currently working F# packages, but installing a whole system from unstable has the sorts of stability issues you might expect, and cherry-picking the right .deb packages from the Debian repositories is unpleasant. There's also the option of using an F# developer's personal repository (https://gist.github.com/tkellogg/5619461), but I don't like adding untrusted sources to my sources.list.

After discovering that Vagrant includes support for a version of Debian Wheezy with F#, I figured out a working, relatively uninvasive approach based on the package

@csgordon
csgordon / gist:5846399
Last active December 18, 2015 21:19
Setting up Microsoft Research's F* compiler

Setting up MSR's F* Compiler on Windows, for use under Cygwin.