chadbrewbaker

Chrome UTF-8 Decoder

NGINX UTF-8 Javascript

Chrome UTF-8 DFA

Rust UTF-8 Decoder/validator

MUSL mbrtowc

bencbartlett

<< MaTeX`
SetOptions[MaTeX, "Preamble" -> {"\\usepackage{color,txfonts}"}];
SetDirectory[NotebookDirectory[]];

Clear[drawLadder];
drawLadder[n_, l_, m_, imsize_: 500] := Module[{maxrungs = 5, mag = 4},
   Graphics[{
     White, Opacity[1], Thickness[.02], Dashing[None],
     Table[Line[{{0, k}, {1, k}}], {k, maxrungs}], (*draw n lines*)
  

johnchandlerburnham

I: Type
  i<P: (i:I) -> Type> ->
  (I0: P(I.0)) ->
  (I1: P(I.1)) ->
  (IE: Path(P, I0, I1)) ->
  P(i)

I.0: I
  <P> (i0) (i1) (ie) i0

akhtarraza

//Reference: https://stackoverflow.com/questions/53906275/rsa-public-key-created-in-ios-swift-and-exported-as-base64-not-recognized-in-jav

import SwiftyRSA

class RSAKeyEncoding: NSObject {
    
    // ASN.1 identifiers
    private let kASNBitStringIdentifier: UInt8 = 0x03
    private let kASNSequenceIdentifier: UInt8 = 0x30
    

Gabriella439

-- Credit to: https://news.ycombinator.com/item?id=15186988

let iterate
    : (Natural → Natural) → Natural → Natural
    =   λ(f : Natural → Natural)
      → λ(n : Natural)
      → Natural/fold (n + 1) Natural f 1

let increment : Natural → Natural = λ(n : Natural) → n + 1

hfossli

//
//  ASN1.swift
//  ASN1
//
//  Created by Håvard Fossli on 29.08.2018.
//  Copyright © 2018 Håvard Fossli. All rights reserved.
//

import Foundation

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

jozefg

module mltt where
open import Data.Nat
import Data.Fin as F
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

data Tm : ℕ → Set where
  var   : ∀ {n} → F.Fin n → Tm n

bryc

DX7

Note: One of the algorithms is incorrect due to a missing operator. Need to update the image. Will have to get on that soon.

These are the original 32 algorithms as used in Yamaha DX7.

The later Yamaha FS1R and Yamaha SY77 may have compatibility with these algorithms, but that's beyond the current scope. The FS1R contains 88 algorithms, while the SY77 contains 45 algorithms.

esmolanka

import prelude
import equiv

data nat
  = zero
  | suc (n : nat)

data fix (f : U -> U) = mk (x : f (fix f))

data maybe (A : U)