Instructions are modified from emacs-w64 Wiki page by zklhp. Many thanks for sharing!
Download the latest MSYS2 from this download page.
Install MSYS2 to, for example, C:\msys2 (make sure no space in path to avoid unwanted problems).
Optionally prettify the MSYS2 console mintty with ~/.minttyrc to make it more pleasing to eyes. Thanks to this awesome theme!
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.
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.
| #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 | |
(draft; work in progress)
See also:
| #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. |
| #lang racket/base | |
| (require racket/match) | |
| (provide current-solver-path | |
| call-with-solver | |
| solve) | |
| (define current-solver-path (make-parameter (find-executable-path "z3"))) |
| #!/usr/bin/env scheme --script | |
| (import (nanopass)) | |
| (define unique-var | |
| (let () | |
| (define count 0) | |
| (lambda (name) | |
| (let ([c count]) | |
| (set! count (+ count 1)) |
