leque

type t =
  | Leaf of int * string
  | Concat of int * t * t

let length = function
  | Leaf (i, _) -> i
  | Concat (i, _, _) -> i

let leaf s =
  Leaf (String.length s, s)

leque

type t =
  | Leaf of int * string
  | Concat of int * t * t

let length = function
  | Leaf (i, _) -> i
  | Concat (i, _, _) -> i

let leaf s =
  Leaf (String.length s, s)

leque

;;; Gaucheの拡張文字クラス
(use util.match)

(pprint
 (let ()
   (define f
     (match-lambda
       ((name actual expected)
        (let ((b (equal? actual expected)))
          (and (not b) (list name b))))))

leque

;;
;; Scheme 9 from Empty Space
;; Copyright (C) 2007 Nils M Holm <[email protected]>
;;

;;----- Library -----

(define (not x) (eq? #f x))

(define number? integer?)

leque

# cd opam-repository
# ruby hoge.rb packages/*

def ocaml_ver_lower_bound(dir)
   File.read(File.join(dir, 'opam')).lines.collect {|line|
      / *"ocaml" {>= "([^"]*)".*$/.match(line){|m| m[1] }
   }.detect{|x| x }
end

def latest_dir(package)

leque

Require Extraction.
(* https://coq.github.io/doc/master/stdlib/Coq.Arith.Factorial.html *)
Require Import Coq.Arith.Factorial.

Extraction Language JSON.
Extraction fact.
(*
{
  "what": "decl:fixgroup",
  "fixlist": [

leque

Require Extraction.

Inductive list (A : Type) : Type :=
 | nil : list A
 | cons : A -> list A -> list A.

CoInductive Stream (A : Type) :=
  Cons : A -> Stream A -> Stream A.

Extraction Language Haskell.

leque

(use srfi-1)
(use util.match)

(define id-cont
  `(lambda (x) x))

(define (translate term env cont)
  (match term
    ((? integer? term)
     `(,cont ,term))

leque

ℰ : Exp -> Env -> Cont -> Ans
Proc = Val -> Cont -> Ans
ρ ∈ Env = Var -> Val
κ ∈ Cont = Val -> Ans

ℰ⟦x⟧ρκ = κ (ρ⟦x⟧)
ℰ⟦E1 E2⟧ρκ = ℰ⟦E1⟧ρ (λf. ℰ⟦E2⟧ρ (λa. f a κ)
ℰ⟦λx.E⟧ρκ = κ (λv.λκ'. ℰ⟦E1⟧ρ[⟦x⟧↦v]κ')
ℰ⟦Sk.E⟧ρκ = ℰ⟦E⟧ρ[⟦k⟧↦λv.λκ'.κ' (κ v)] (λx. x)
ℰ⟦<E>⟧ρκ = κ (ℰ⟦E⟧ρ(λx. x))

leque

#include QMK_KEYBOARD_H

extern keymap_config_t keymap_config;

// Each layer gets a name for readability, which is then used in the keymap matrix below.
// The underscores don't mean anything - you can have a layer called STUFF or any other name.
// Layer names don't all need to be of the same length, obviously, and you can also skip them
// entirely and just use numbers.
#define _QWERTY 0
#define _COLEMAK 1