nyuichi

// the characteristic of the diagonal mono δ : α → α × α
constant eq : α → α → Prop

infix = : 50 := eq

// This is definitionally equal to any term of the Unit type by the eta rule.
constant star : Unit

/-
This introduces a constant `top` and:

nyuichi

The make command hangs up when it is run as init (PID=1) and its child processes are terminated with SIGINT

$ ls
loop.sh  Makefile  run-loop.sh
$ cat loop.sh 
#!/bin/bash
trap 'echo SIGTERM && exit 0' SIGTERM
trap 'echo SIGINT && exit 0' SIGINT
while true; do :; done

nyuichi

! [Type Error] at "bug.saty", line 11, character 0 to line 15, character 3:
    The implementation of value 'make' has type
      ('a phantom) M.t
    which is inconsistent with the type required by the signature
      ('#a phantom) M.t

nyuichi

; -*- mode: scheme;-*-
; Implementation of resolution principle for first-order logic in Egison

(define $unordered-pair
 (lambda [$m]
  (matcher
    {[<pair $ $> [m m] {[[$x $y] {[x y] [y x]}]}]
     [$ [something] {[$tgt {tgt}]}]})))

(define $positive?

nyuichi

(use r7rs)

(define uniq
  (let ((n 0))
    (lambda ()
      (set! n (+ n 1))
      (string->symbol (string-append "$" (number->string n))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; - Operational aspects of untyped normalization by evaluation, K. Aehlig et al, MSCS 2003.

nyuichi

import data.set
open function

universes u
variables {α β γ : Type u} 

noncomputable def bijective_inv (f : α → β) (h : bijective f) (b : β) : α :=
classical.some (h.right b)

lemma bijective_inv_spec (f : α → β) (h : bijective f) (b : β) : f (bijective_inv f h b) = b :=

nyuichi

open eq

section eckmann_hilton
  universe variables u
  parameter {α : Type u}
  parameters plus mult : α → α → α
  parameters one zero : α
  local notation a + b := plus a b
  local notation a * b := mult a b

nyuichi

import Chisel._

class SdramController extends Module {

  val io = new Bundle {
    val a = Bits(OUTPUT, 13)
  }

  io.a := UInt(0)
  io.a(10) := Bool(true)

nyuichi

;;; data Comonad f a where
;;;   Comonad a ((Comonad f a -> b) -> f b)

; counit : Comonad f a -> a
; cobind : Comonad f a -> (Comonad f a -> b) -> Comonad f b

; lift : (f a -> a) -> (f a -> (f a -> b) -> f b) -> (f a -> Comonad f a)
; run  : Comonad f a -> f a

(define Comonad cons)

nyuichi

(import (gauche partcont)
        (scheme base)
        (scheme write))


;;; generic fmap

(define *fmap-methods*
  `((,list? . ,map)))