type Nat = 0 | { succ: Nat };
type Succ<N extends Nat> = { succ: N };
type Prev<N extends Nat> =
N extends Succ<infer M> ? M : N;
type Add<N extends Nat, M extends Nat> =
N extends Succ<infer PrevN> ? { succ: Add<PrevN, M> } : M;
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
B = build | |
$B/%.o: %.cpp | $B | |
$(CXX) $(CXXFLAGS) $(INCLUDE) -o $@ -c $< | |
$B/%.debug.o: %.cpp $B | |
$(CXX) $(CXXFLAGS) $(INCLUDE) -o $@ -c $< | |
%.exe: %.o | |
$(CXX) $(CXXFLAGS) $(LDFLAGS) -o $@ $^ |
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
# Edit this configuration file to define what should be installed on | |
# your system. Help is available in the configuration.nix(5) man page | |
# and in the NixOS manual (accessible by running ‘nixos-help’). | |
{ config, pkgs, lib, ... }: | |
{ | |
imports = | |
[ ./hardware-configuration.nix | |
./thinkpad.nix |
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
if x1 then | |
1 | |
else if x2 then | |
2 | |
else if x3 then | |
3 | |
if x1 then | |
1 |
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
let get = function | |
| Some x -> x | |
| None -> raise Not_found | |
let with_default def = function | |
| Some x -> x | |
| None -> def | |
let map f = function | |
| Some x -> Some (f x) |
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
FILES= coreexamples.tex lablexamples.tex objectexamples.tex moduleexamples.tex\ | |
advexamples.tex polymorphism.tex | |
TOPDIR=../../.. | |
include $(TOPDIR)/Makefile.tools | |
LD_PATH="$(TOPDIR)/otherlibs/str:$(TOPDIR)/otherlibs/unix" | |
CAMLLATEX=$(SET_LD_PATH) $(OCAMLRUN) ../../tools/caml-tex2 | |
TEXQUOTE=../../tools/texquote2 |
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
#!/usr/bin/env rc | |
dir=$home/Desktop | |
cd /tmp | |
printf 'Cloning Textual... ' | |
git clone -q 'https://github.com/Codeux-Software/Textual.git' | |
echo Done! | |
printf 'Cloning submodules... ' | |
cd Textual |
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
[0;37;5;47;107m . . . . . . . . . . . . . . . . . . [0m | |
[0;37;5;47;107m . . . . . . . . . . . . . . . . .. . . . . . . [0m | |
[0;37;5;47;107m . . . . . . . . . . . ..:[0;1;37;97;47mX;[0;37;5;47;107mS.. . . . . . [0m | |
[0;37;5;47;107m . . . . . . . . . . . .%[0;1;37;97;47mX[0;1;30;90;47m %[0;37;5;40;100m8[0;1;30;90;47mtt[0;37;5;40;100m8[0;1;30;90;47m.[0;1;37;97;47mX[0;37;5;47;107m.. . . . . .[0m | |
[0;37;5;47;107m . . . . . . . . . . . . t[0;1;37;97;47m@:[0;1;30;90;47m;@SS%t[0;1;30;90;45m8[0;1;30;90;47m.[0;35;47m8[0;1;30;90;47m;X%[0;37;5;47;107m@:. . . . . [0m | |
[0;37;5;47;107m . . . . . . . . . . ..%[0;1;37;97;47m [0;1;30;90;47mS[0;37;5;40;100m8[0;1;30;90;47m%StS[0;37;45m8[0;1;30;90;47mS[0;1;30;90;45m8[0;1;30;90;47m ;tS[0;35;47m8[0;1;30;90;47mS%[0;35;5;40;100m:[0;1;37;97;47m;[0;37;5;47;107 |
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
require 'twitter' | |
client = Twitter::REST::Client.new do |config| | |
config.consumer_key = "" | |
config.consumer_secret = "" | |
config.access_token = "" | |
config.access_token_secret = "" | |
end | |
if ARGV[1].nil? |
This document defines how manga releases hosted on The Helvetica Scenario and the files inside them have to be named.
This is to avoid a cluserfuck of filenames, which only makes the user experience worse and makes finding files a mess.
The chapter archives (which should always be compressed in .zip as it's ubiquitous and open source) have to be named using this scheme:
Series Name v04c32x1 [Group Name]{r2}.zip
The elements mentioned in this example will be explained here:
NewerOlder