shhyou

#lang racket/base

(require racket/match)

(provide current-solver-path
         call-with-solver
         solve)

(define current-solver-path (make-parameter (find-executable-path "z3")))

soegaard

#lang racket/base
(provide uniq)

;;;
;;; Uniq
;;; 

; The function uniq takes a list as input and returns a new list:
; adjacent elements are compared and omits any repeated elements.
; In other words, uniq works like the Unix utility uniq, but on list.

swatson555

#!/usr/bin/env scheme --script

(import (nanopass))

(define unique-var
  (let ()
    (define count 0)
    (lambda (name)
      (let ([c count])
        (set! count (+ count 1))

soegaard

#lang racket
;; adapted from:
;; https://planet.racket-lang.org/package-source/dyoo/sicp-concurrency.plt/1/2/sicp-concurrency.ss
;; concurrency: SICP concurrency primitives
;; adapted from http://list.cs.brown.edu/pipermail/plt-scheme/2002-September/000620.html
  
;;; Sources:
;;; Dorai Sitaram, "Learn Scheme in a Fixnum of Dayes", chapter 15
;;; Dyvig, http://www.scheme.com/tspl2d/examples.html#g2433
    

MarisaKirisame

type expr =
| Var of string
| Int of int
| Add of (expr * expr)
| Mult of (expr * expr)
| Let of (string * expr * expr)
| IfZero of (expr * expr * expr)
| Pair of (expr * expr)
| Zro of expr
| Fst of expr

paulcadman

Types are theorems, programs are proofs.

(The code examples here use idris https://www.idris-lang.org)

To augment testing with a finite number of inputs we write mathematical proofs that demonstrate their correctness on all possible inputs.

The programmer writes the proofs and the compiler checks the proofs as it builds the software.

andregrigon

How to Debug Chez Scheme Programs

R. Kent Dybvig

August 2002

1. Basic debugging techniques
   1. Kinds of failure
   2. Understanding error messages
   3. Staring at the code
2. Simplifying the code and input

larvata

ffmpeg Cheatsheet

-loglevel debug

• Join TS Files
• Convert TS to MP4
• Download Online AES-128 Encrypted HLS video
• Convert Video to GIF

nauhygon

Build Emacs-w64 with MSYS2/MinGW-w64 with Native Compilation

Instructions are modified from emacs-w64 Wiki page by zklhp. Many thanks for sharing!

1. Download the latest MSYS2 from this download page.

2. Install MSYS2 to, for example, C:\msys2 (make sure no space in path to avoid unwanted problems).

3. Optionally prettify the MSYS2 console mintty with ~/.minttyrc to make it more pleasing to eyes. Thanks to this awesome theme!

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.