Title | Author(s) | Year |
---|---|---|
Intuitionistic Type Theory | Per Martin-Löf | 1984 |
On the Meanings of the Logical Constants and the Justification of the Logical Laws | Per Martin-Löf | 1996 |
[[http://mat.uab.cat/~kock/crm/h |
This file contains hidden or 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
# | |
# Example of how to render an ascii tree from a parent vector | |
# | |
Draw⇐{ | |
d←(⊢∾1+⊏⟜⥊)´⌽p←𝕩 # p: parent vector, d: depth vector | |
w←{∾⍟(1-˜≡)(𝕨(⊣⊔˜⊏)p)⊸(⊢∾¨⊏˜)⌾((𝕩∊𝕨⊏p)⊸/)𝕩}´⌽d⊔↕≠p # order depths depending on parent groups | |
n←(1+w⊏p)⊸∧˘(1+⌈´d)↑w=⌜w⊏d # matrix of ordered depth path cut off | |
n↩(0≠∨˝n)⊸/˘n↩>(↕≠)⊸({«⍟𝕨 𝕩}˘)n # shift columns under parent node and remove empty space | |
s←0<∊⊸∧˘n⋄e←0<(⌽∘∊∘⌽)⊸∧˘n⋄h←s+`∘-˘e⋄m←0<h∧n⋄v←s∧e # s: start, e: ends, h: horizontals, m: middles, v: verticals | |
b←" ─┬├┐│"⊏˜(0⥊˜≠⍉n)∾1↓⌈´h‿m‿s‿e‿vר1+↕5 # branches - nullify root layer. 1: horizontal, 2: middle, 3: start, 4: end, 5: vertical, |
This file contains hidden or 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
n←•BQN∾{"{"∾𝕩∾"}"} (↕≠d){ ∾⟨𝕩,"⇐",•Fmt𝕨,","⟩ }¨ d←"foo"‿"bar" |
This file contains hidden or 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
# Reference: https://www.instantdb.com/essays/datalogjs | |
db←[ | |
⟨"100", "person/name", "James Cameron"⟩, | |
⟨"100", "person/born", "1954-08-16T00:00:00Z"⟩, | |
⟨"101", "person/name", "Arnold Schwarzenegger"⟩, | |
⟨"101", "person/born", "1947-07-30T00:00:00Z"⟩, | |
⟨"102", "person/name", "Linda Hamilton"⟩, | |
⟨"102", "person/born", "1956-09-26T00:00:00Z"⟩, | |
⟨"103", "person/name", "Michael Biehn"⟩, |
This file contains hidden or 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
#include <stdio.h> | |
#include <stdlib.h> | |
#include <string.h> | |
#include <errno.h> | |
#include <termios.h> | |
#include <unistd.h> | |
#include <wchar.h> | |
#include <locale.h> | |
#include "replxx.h" | |
#include "sqlite3.h" |
This file contains hidden or 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
string ← •Import "string.bqn" | |
# Poor mans templating engine | |
Fmt←{ 𝕨⊸string.Fmt¨<˘𝕩} | |
foo←∾∾⟨ | |
"<div>" | |
"<span>{value}</span>" Fmt ↕10 | |
"<span class='{0}'>{1}</span>" Fmt [⟨"foo",1⟩,⟨"bar",2⟩] |
This file contains hidden or 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
Bytecode: ⟨ 0 1 33 0 0 48 6 0 1 0 0 34 0 0 17 7 ⟩ | |
Loc: ⟨ ⟨ 2 2 0 0 0 1 3 6 6 5 5 4 4 4 5 4 ⟩ ⟨ 2 2 0 0 0 1 3 6 6 5 5 4 4 4 5 4 ⟩ ⟩ | |
Token: | |
┌─ | |
· ⟨ 95 72 96 64 95 0 96 ⟩ ⟨ 0 ¯3 0 ¯1 0 1 0 ⟩ ⟨ ⟨ "a" ⟩ ⟨⟩ ⟨ 2 ⟩ ⟨⟩ ⟨⟩ ⟩ ⟨ 0 1 2 3 4 5 6 ⟩ ⟨ 0 1 2 3 4 5 6 ⟩ | |
┘ |
This file contains hidden or 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
lib.so: lib.c | |
gcc -shared lib.c -o lib.so |
This file contains hidden or 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
Date | Description | Credit | Debit | Balance | |
---|---|---|---|---|---|
26/02/2024 | Foo Bar Baz Card 12345xxxxxx5678 | -11.19 | 2017.05 | ||
26/02/2024 | Foo Bar Baz Card 12345xxxxxx5678 | -11.19 | 2017.05 | ||
26/02/2024 | Foo Bar Baz Card 12345xxxxxx5678 | -11.19 | 2017.05 | ||
26/02/2024 | Foo Bar Baz Card 12345xxxxxx5678 | -11.19 | 2017.05 | ||
26/02/2024 | Foo Bar Baz Card 12345xxxxxx5678 | -11.19 | 2017.05 | ||
26/02/2024 | Foo Bar Baz Card 12345xxxxxx5678 | -11.19 | 2017.05 | ||
26/02/2024 | Foo Bar Baz Card 12345xxxxxx5678 | -11.19 | 2017.05 | ||
26/02/2024 | Foo Bar Baz Card 12345xxxxxx5678 | -11.19 | 2017.05 | ||
26/02/2024 | Foo Bar Baz Card 12345xxxxxx5678 | -11.19 | 2017.05 |
This file contains hidden or 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
import std.stdio; | |
import std.uni; | |
import std.conv; | |
///Taken from https://github.com/dlang/dmd/blob/0517fc93ceb9e74e979bbbc9de64eb64d610094c/src/dmd/utf.d | |
static immutable wchar[2][] ALPHA_TABLE = | |
[ | |
[0x00AA, 0x00AA], | |
[0x00B5, 0x00B5], | |
[0x00B7, 0x00B7], | |
[0x00BA, 0x00BA], |
NewerOlder