astahfrom

theory THM0_741 imports Main begin

datatype 'a s  = S 'a

datatype 'a t = T ‹'a s›

primrec f :: ‹'a s ⇒ 'a set› where
  ‹f (S x) = {x}›

primrec g :: ‹'a t ⇒ 'a set› where

astahfrom

theory QuickSort imports Main begin

fun quicksort :: "('a :: ord) list ⇒ 'a list" where
  "quicksort [] = []"
| "quicksort (x#xs) = (
    let (smaller, greater) = partition (op ≥ x) xs
    in quicksort smaller @ x # quicksort greater)"

lemma quicksort_content: "set xs = set (quicksort xs)"
proof (induct xs rule: quicksort.induct)

astahfrom

use std::marker::PhantomData;

type Is<S, T> = Is_<S, T>;

#[derive(Clone)]
struct Is_ <S, T>(PhantomData<S>, PhantomData<T>);

fn refl<T>() -> Is<T, T> {
    Is_(PhantomData, PhantomData)
}

astahfrom

make  check-TESTS
make[5]: Entering directory '/private/var/folders/f7/41q7cy8928scch2rrqtncdqr0000gn/T/nix-build-texlive-core-2014.drv-0/texlive-bin-2014.20140926.35254/Work/texk/web2c'
make[6]: Entering directory '/private/var/folders/f7/41q7cy8928scch2rrqtncdqr0000gn/T/nix-build-texlive-core-2014.drv-0/texlive-bin-2014.20140926.35254/Work/texk/web2c'
PASS: tangle.test
PASS: bibtex.test
PASS: dvicopy.test
PASS: dvitype.test
PASS: gftodvi.test
PASS: gftopk.test
PASS: gftype.test

astahfrom

{ config, pkgs, ... }:

{
  imports = [ ./hardware-configuration.nix ];

  boot.kernelModules = [ "applesmc" ];

  boot.cleanTmpDir = true;
  boot.loader = {
    gummiboot.enable = true;

astahfrom

if test -n $HOME
  set NIX_LINK "$HOME/.nix-profile"

  # Set the default profile
  if test ! -L "$NIX_LINK"
    echo "creating $NIX_LINK" >&2
    set _NIX_DEF_LINK /nix/var/nix/profiles/default
    /nix/store/4yn9bxlscdvbzjmdkhfnxd9a3jm8phns-coreutils-8.23/bin/ln -s "$_NIX_DEF_LINK" "$NIX_LINK"
  end