siraben

(* Instead of using the Real library's sqrt and spec, we give a proof
   from first principles following the same argument given in a
   lecture early on in my Introduction to Analysis class, using the
   completeness property and some order theory.  *)

Require Import Reals.
Require Import Psatz.

Open Scope R_scope.

siraben

From Coq.Arith Require Import PeanoNat.
Import Nat.
Require Import Lia.

Definition add_mod n i j :=
  match i + j ?= n with
  | Lt => i + j
  | _ => i + j - n
  end.

siraben

#!/bin/bash
# SPDX-License-Identifier: MIT
# SPDX-FileCopyrightText: 2018 Ben Siraphob <bensiraphob@gmail.com>
command -v gshuf >/dev/null 2>&1 || { echo >&2 "gshuf is required but is not installed.  Run \"brew install coreutils\"."; control_c; }
command -v spoof-mac >/dev/null 2>&1 || { echo >&2 "spoof-mac is required but is not installed.  Run \"brew install spoof-mac\"."; control_c; }

# Colors
RED='\033[0;31m'
NC='\033[0m'

siraben

Clarifying GPL license variant with upstream packages

Title of the post:

Clarify GPL license variant

Could you clarify which GPL variant this software is packaged under? For more info, see this website.

Summary:

The Free Software Foundation urged developers to choose or any later version, since that meant users would be free to use that program under GNU GPL version 1, or under version 2 (once there was a version 2), or under version 3 (once there was a version 3). And they will be free to use it under version 4, if we ever have to make a version 4.

siraben

{ pkgs ? import <nixpkgs> {} }:
with pkgs;

qt5.callPackage ./rmview.nix { }

siraben

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
import Prelude (Bool,Show, (+))
import qualified Prelude as P
import Control.Arrow
import Control.Monad
import Control.Category

data s :. a = s :. a

siraben

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE BangPatterns #-}
-- nix-shell --pure -i ghci -p "haskellPackages.ghcWithPackages (h: [ h.QuickCheck ])"

import Data.List
import Control.Monad

-- https://leetcode.com/problems/longest-mountain-in-array/

data Dir = Up | Down | Flat deriving (Show)

siraben

#! /usr/bin/env nix-shell
#! nix-shell --pure -i ghci -p "haskellPackages.ghcWithPackages (h: [ h.QuickCheck ])"

-- https://leetcode.com/problems/binary-tree-tilt/

import Test.QuickCheck

data Tree = Node Int Tree Tree | Leaf deriving (Show)

instance Arbitrary Tree where

siraben

Evals report

Report built at 2020-11-22 08:27:35 UTC

Built for evals:

• 1628912

---

siraben

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
-- Tuesday, September 15, 2020 at 16:20
-- Lambda calculus with de Bruijn representation in tagless-final
-- style

-- Just so that we can write repr γ ⊢ a -> repr γ ⊢ b, etc.
infix 3 ⊢
type a ⊢ b = a b