bobatkey

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

module tuple where





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

AndrasKovacs

{-# language
  BlockArguments
, ConstraintKinds
, ImplicitParams
, LambdaCase
, OverloadedStrings
, PatternSynonyms
, Strict
, UnicodeSyntax
#-}

neel-krishnaswami

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

Trebor-Huang

{-# 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?

Trebor-Huang

{-# OPTIONS --cubical --no-import-sorts --postfix-projections -W ignore #-}
module freeCCC where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Unit using (Unit; isPropUnit; isSetUnit)
open import Cubical.Data.Bool using (Bool; true; false; if_then_else_; isSetBool)
open import Cubical.Data.Sum using (_⊎_; inr; inl)
open import Cubical.Data.Sigma using (Σ; _×_; ΣPathP)

typeswitch-dev

#include <stdio.h>
#include <string.h>
#include <assert.h>
FILE *in; long M[1<<24]={0}, *D, *R, H=0x130000, IP=0, T;
long getu() { long t, h =  getc(in);         if (h < 0xC0) return h;
    t = ((h&0x1F) << 6) | (getc(in) & 0x3F); if (h < 0xE0) return t;
    t = ( t       << 6) | (getc(in) & 0x3F); if (h < 0xF0) return t;
    t = ( t       << 6) | (getc(in) & 0x3F); return t & 0x1FFFFF; }
void putu(long c) { if (c < 0x80) { putchar(c); return; }
    if (c < 0x7FF) { putchar(0xC0|(c>>6)); } else {

AndrasKovacs

{-# language LambdaCase, Strict, BangPatterns, ViewPatterns, OverloadedStrings #-}
{-# options_ghc -Wincomplete-patterns #-}

module UnivPoly where

import Data.Foldable
import Data.Maybe
import Data.String
import Debug.Trace

shhyou

;; Exporting free identifier table operations that close over a global map
#lang racket/base

(require racket/list
         syntax/id-table)

(provide env-ref env-has-id? env-add!)

(define id-table (make-free-id-table))

ice1000

{- Lean 4
open list
#eval filter (= 4) [1, 2, 4]
-}

open import Data.Nat renaming (ℕ to Nat; _≟_ to decEqNat)
open import Data.List using (List; []; _∷_)
open import Data.Bool using (true; false)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

lynn

module PrettyParseError (
    prettyParseError,
    PrettyParseErrorOptions(PrettyParseErrorOptions),
    prettyParseErrorDefaults
) where

import Data.List (intercalate, nub)
import Text.Parsec
import Text.Parsec.Error
import Text.Parsec.Pos