siraben

(require 'package)
(let* ((no-ssl (and (memq system-type '(windows-nt ms-dos))
                    (not (gnutls-available-p))))
       (proto (if no-ssl "http" "https")))
  ;; Comment/uncomment these two lines to enable/disable MELPA and MELPA Stable as desired
  (add-to-list 'package-archives (cons "melpa" (concat proto "://melpa.org/packages/")) t)
  ;;(add-to-list 'package-archives (cons "melpa-stable" (concat proto "://stable.melpa.org/packages/")) t)
  (when (< emacs-major-version 24)
    ;; For important compatibility libraries like cl-lib
    (add-to-list 'package-archives '("gnu" . (concat proto "://elpa.gnu.org/packages/")))))

siraben

with import <nixpkgs> {};


lib.fix (self: {
  z80e = stdenv.mkDerivation {
     name = "z80e";
     src = fetchurl {
       url = "https://github.com/KnightOS/z80e/archive/0.4.0.tar.gz";
       sha256 = "b8940393bfff843ef26b2f43770a9d7e8cb0601f67804571b238bbca52919e7d";
     };

siraben

VARIABLE HANDLER

0 HANDLER !

: CATCH ( xt -- exception# | 0      \ return addr on stack )
   SP@ >R	            ( xt )  \ save data stack pointer
   HANDLER @ >R	      ( xt )        \ and previous handler
   RP@ HANDLER !	     ( xt ) \ set current handler
   EXECUTE	           ( )      \ execute returns if no THROW
   R> HANDLER !	      ( )           \ restore previous handler

siraben

: ENTER >R ;
: SUCC ' R@ , ' ENTER , ; IMMEDIATE
: FAIL ' R> , ' DROP , ' EXIT , ; IMMEDIATE

: RANGE
  1+ >R 1-
  CREATE
  ' LIT ,
  ,
  POSTPONE BEGIN

siraben

with import <nixpkgs> {};

lib.fix (self: {
  tilp = stdenv.mkDerivation {
     name = "tilp";
     src = fetchurl {
       url = "https://www.ticalc.org/pub/unix/tilp.tar.gz";
       sha256 = "1mww2pjzvlbnjp2z57qf465nilfjmqi451marhc9ikmvzpvk9a3b";
     };
     nativeBuildInputs = [ autoreconfHook automake ];

siraben

Inductive day : Type :=
 | monday
 | tuesday
 | wednesday
 | thursday
 | friday
 | saturday
 | sunday.

Definition next_weekday (d:day) : day :=

siraben

Require Import Omega.
Require Import Extraction.

(* Inductive binary number data type. *)
Inductive bin : Type :=
 | Z
 | A (n : bin)
 | B (n : bin).

siraben

;; Monadic parsing in Scheme

(use-modules (ice-9 match)
             (ice-9 binary-ports)
             (rnrs bytevectors)
             (ice-9 textual-ports)
             (srfi srfi-9))

;; Helper procedures `compile-port' and `emit' for output.
(define compile-port

siraben

module Nat exposing (..)

-- Example of inductively defined data type.
type Nat = O | S Nat

toNat : Int -> Nat
toNat n = case n of
            0  -> O
            sn -> S (toNat (sn - 1))

siraben

(use-modules (ice-9 match))
;; An actor is a computational entity that, in response to a message
;; it receives, can concurrently:

;; send a finite number of messages to other actors;
;; create a finite number of new actors;
;; designate the behavior to be used for the next message it receives.

;; So it's a dispatch of sorts.