| {-# language BlockArguments, LambdaCase, Strict, UnicodeSyntax #-} | |
| {-| | |
| Minimal dependent lambda caluclus with: | |
| - HOAS-only representation | |
| - Lossless printing | |
| - Bidirectional checking | |
| - Efficient evaluation & conversion checking | |
| Inspired by https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196 |
| type term = | |
| | Lam of (term -> term) | |
| | Pi of term * (term -> term) | |
| | Appl of term * term | |
| | Ann of term * term | |
| | FreeVar of int | |
| | Star | |
| | Box | |
| let unfurl lvl f = f (FreeVar lvl) |
original url - https://www.facebook.com/notes/daniel-colascione/buttery-smooth-emacs/10155313440066102/
30 October 2016
Public Emacs has flickered for 30 years. Now, it should be flicker-free. I’ve just landed support for double-buffered rendering for the X11 port. Now you should be able to edit, resize, and introduce bugs in your awful codebase without seeing a partially-rendered buffer or being incited to murder by barely-perceptible white flashes while editing that
| trait Interp { | |
| type Repr<T>; | |
| fn lit(i: i32) -> Self::Repr<i32>; | |
| fn add(a: Self::Repr<i32>, b: Self::Repr<i32>) -> Self::Repr<i32>; | |
| } | |
| struct Eval; | |
| impl Interp for Eval { |
| ``` | |
| OCaml compilation pipeline | |
| ┌────────────────┐ | |
| │ │ | |
| │ Source code │ |
| (* The syntax of our calculus. Notice that types are represented in the same way | |
| as terms, which is the essence of CoC. *) | |
| type term = | |
| | Var of string | |
| | Appl of term * term | |
| | Binder of binder * string * term * term | |
| | Star | |
| | Box | |
| and binder = Lam | Pi |
| module Data.DepPath | |
| import Data.Nat | |
| import Data.Vect | |
| ||| Equivalent to the built-in `replace`. | |
| public export | |
| transport1 : (0 a0 : Type) | |
| -> (0 a1 : a0 -> Type) | |
| -> (0 x0 : a0) |
| /** | |
| * Get lost unsaved buffers in Atom editor | |
| * | |
| * Load text content of all unsaved buffers stored by Atom for any project in IndexedDB and print it to Developers tools console | |
| * | |
| * Author: David Ferenczy Rogožan (https://ferenczy.cz) | |
| * | |
| * Instructions: | |
| * | |
| * 1. Start Atom |
| module Container | |
| %default total | |
| record Container where | |
| constructor MkContainer | |
| shape : Type | |
| position : shape -> Type | |
| container : Container -> Type -> Type |
