rzrn

{-# OPTIONS --cubical #-}
module Experiments where

open import Agda.Builtin.Cubical.Path public
open import Agda.Builtin.Cubical.Sub public renaming (primSubOut to ouc)
open import Agda.Primitive.Cubical public
  renaming ( primIMin       to _∧_  -- I → I → I
           ; primIMax       to _∨_  -- I → I → I
           ; primINeg       to -_   -- I → I
           ; isOneEmpty     to empty

rzrn

type expr =
  | EVar of string
  | EApp of expr * expr
  | EPi of string * expr * expr
  | ESig of string * expr * expr
  | ELam of string * expr * expr
  | EPair of expr * expr
  | EFst of expr
  | ESnd of expr
  | ESet of int

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