dannypsnl

{-# OPTIONS --postfix-projections #-}

module tuple where





------------------------------------------------------------------------------
--

dannypsnl

{-# language
  BlockArguments
, ImplicitParams
, LambdaCase
, OverloadedStrings
, PatternSynonyms
, Strict
, UnicodeSyntax
#-}
{-# options_ghc -Wincomplete-patterns -Wunused-imports #-}

dannypsnl

module C : sig
  type t 
  val empty : t 
  val one : char -> t 
  val union : t -> t -> t 
  val inter : t -> t -> t 
  val top : t 
  val mem : char -> t -> bool 
  val make : (char -> bool) -> t 
  val equal : t -> t -> bool

dannypsnl

{-# OPTIONS --cubical #-}
module natmod where
open import Cubical.Foundations.Prelude

data Ctx : Type
data _⊢_ : Ctx → Ctx → Type
data Ty : Ctx → Type
data Tm : Ctx → Type
-- This is halfway between EAT and GAT.
-- GAT is hard! Why is EAT so easy?

dannypsnl

module Main

data Expr = E

data Stmt
  = If Expr Stmt Stmt -- if (condition) then A else B
  -- loop (condition):
  --   do xxx
  | Loop Expr Stmt
  | SE String

dannypsnl

module Main

import Control.App
import Control.App.Console
import Data.SortedSet

data Op = Add | Sub | Mul | Div

data Expr
  = Var String

dannypsnl

{-# LANGUAGE LambdaCase #-}

module Tyck
  ( Term (..),
    Type (..),
    emptyContext,
    emptySolution,
    topInfer,
    infer,
    check,

dannypsnl

#lang racket

(define prime-list '(2 3 5 7 11 13 17 19 23 29 31 37 41 43 47 53 59))

(define (factor-list n)
  (define p-factor-list
    (for/list ([p prime-list]
               #:when (= (remainder n p) 0))
      p))
  (println p-factor-list)

dannypsnl

#lang racket
(require syntax/parse/define
         (for-syntax syntax/stx))

(begin-for-syntax
  (define-syntax-class type
    #:datum-literals (->)
    (pattern (~literal Type)
      #:attr occurs (λ (D) #f))
    (pattern x:id

dannypsnl

#lang racket/base
(require racket/future
         racket/async-channel
         racket/function
         racket/match)

(define process-map (make-hasheq))
(struct pid ())
(struct process (id fu ch))