lexi-lambda

#lang typed/racket/base

(require (for-syntax racket/base
                     racket/sequence
                     racket/syntax
                     syntax/parse
                     syntax/stx)
         racket/match)

(begin-for-syntax

shhyou

#!/bin/bash
VOLUME=${VOLUME:-0.05}
music_rec="/Volumes/ramdisk/music-rec"
record_file="$music_rec/`pwd | sed -e \"s:$HOME::; s:/Uninterpreted::; s:/:_:g\"`-last_play.txt"
echo Volume filter is $VOLUME.
echo Using record file $record_file.

if [ "$1" == "--reset" ]; then
  echo>"$record_file"
elif [ "$1" != "" ]; then

withzombies

/*
        Copyright (c) 2011, Thomas Dullien
        All rights reserved.

        Redistribution and use in source and binary forms, with or without 
        modification, are permitted provided that the following conditions
        are met:

        Redistributions of source code must retain the above copyright notice,
        this list of conditions and the following disclaimer. Redistributions 

jtanx

[
  {
      "key": "ctrl+shift+tab",
      "command": "workbench.action.previousEditor"
  },
  {
      "key": "ctrl+tab",
      "command": "workbench.action.nextEditor"
  }
]

jespercockx

{-
======================================
=== THE GREAT RESURRECTION OF PROP ===
======================================

Bringing back the impredicative sort Prop of definitionally proof-irrelevant propositions to Agda.

To check this file, get the prop-rezz branch of Agda at https://github.com/jespercockx/agda/tree/prop-rezz.

This file is a short demo meant to show what you currently can (and can't) do with Prop.

pervognsen

Lexicographic comparison for vectors is well known:

x < y iff (x[-1] < y[-1]) | ((x[-1] == y[-1]) & (x[:-1] < y[:-1]))

This corresponds to a serial circuit with a depth linear in the number of elements.

However, it can easily be rewritten in a divide-and-conquer fashion:

x < y iff (x[i:] < y[i:]) | ((x[i:] == y[i:]) & (x[:i] < y[:i]))

shhyou

#lang racket/base

(require racket/contract racket/list racket/match racket/hash)

;; dots ::= ... (literal dots)
;;
;; pattern ::= symbol | boolean | number | string | ,identifier | pattern-list
;; pattern-list ::= () | (pattern . pattern-list)
;;                     | (pattern dots . pattern-list)
;;

L-TChen

{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE TypeInType , ScopedTypeVariables , TypeFamilies, TypeOperators #-} 
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE Safe #-}

module Unification where

import Data.Kind
import Prelude hiding ((++))

andy0130tw

javascript:(H=>{H.replaceState(H.state,null,location.href.replace(/fbclid=[\w\d\-_]+&?/,'').replace(/(\?|&|\?&)$/,''))})(history)

wilbowma

\documentclass{article}

\usepackage{mathpartir}
\usepackage{tikz}

% Play with xshift and yshift if it looks funny
\newcommand{\tikzmark}[1]{\tikz[overlay,remember picture,xshift=-3pt,yshift=1pt] \node (#1) {};}

\begin{document}
\[