CoderPuppy

{-# OPTIONS --overlapping-instances --instance-search-depth=10 #-}

module PHOAS where

open import Agda.Primitive

record Weakening1 {ℓ₁} {ℓ₂} (V : Set ℓ₁) (V' : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  field weaken : V → V'
record Weakening {ℓ₁} {ℓ₂} (V : Set ℓ₁) (V' : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  field weaken : V → V'

CoderPuppy

{-# OPTIONS --without-K #-}

module Berardi where

-- proof irrelevance from impredicativity and excluded middle
-- adapted from https://www.cs.princeton.edu/courses/archive/fall07/cos595/stdlib/html/Coq.Logic.Berardi.html

open import Agda.Primitive

{-# NO_UNIVERSE_CHECK #-}

CoderPuppy

{-# OPTIONS --without-K #-}

module CoquandPaulin where

-- contradiction from non-strictly-positive type and impredicative sigma
-- possibly also "strong elimination", whatever that is
-- and impredicative identity
-- adapted from https://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/
-- originally from Inductively Defined Types by Thierry Coquand and Christine Paulin

CoderPuppy

module Hurkens where

-- derived from https://github.com/agda/agda/blob/5d30d8e7a25dfced02edefd82699f1f7b6f79316/test/Succeed/Hurkens.agda
-- adapted to use impredicativity instead of --type-in-type

data ⊥ : Set where

{-# NO_UNIVERSE_CHECK #-}
record Impred₁ (A : Set₂) (B : A → Set₁) : Set₁ where
  field at : (a : A) → B a

CoderPuppy

{-# OPTIONS_GHC -Wno-tabs #-}
{-# LANGUAGE ImportQualifiedPost, LambdaCase, BlockArguments #-}

module Hemem where

-- roughly Hindley-Milner type inference
-- my first implementation
-- in 1½ hours with no reference
-- just things I pulled from memory (of reading articles about HM)
-- missing an occurs check

CoderPuppy

local I = dofile 'cc/mining/inventory.lua'
xpcall(function()
	dofile 'cc/mining/inventory-ui.lua' (I)
end, function(err)
	if err == 'Terminated' then return end
	sleep(3)
	term.setTextColor(colors.red)
	term.setBackgroundColor(colors.black)
	term.clear()
	term.setCursorPos(1, 1)

CoderPuppy

local fill_i
local fill_left = 0
local function place_fill(f)
	if fill_left <= 0 then
		local is = {}
		for i = 1, 16 do
			local d = turtle.getItemDetail(i)
			if d then
				is[d.name] = is[d.name] or i
			end

CoderPuppy

(use-modules
	(guix profiles)
	(gnu packages idris)
	(guix packages)
	(guix git-download)
	(guix download)
	(guix build-system gnu)
	((guix licenses) #:prefix license:)
	(gnu packages multiprecision)
	(gnu packages llvm)

CoderPuppy

local function refuel(n)
	local sel = turtle.getSelectedSlot()
	local slot = 1
	while turtle.getFuelLevel() < n do
		if slot > 16 then
			error 'no fuel'
		end
		turtle.select(slot)
		if not turtle.refuel(1) then
			slot = slot + 1

CoderPuppy

{-# OPTIONS_GHC -Wno-tabs #-}

module LamCo2 where

import Numeric.Natural

data Term
	= Var Int
	| Lam Term
	| App Term Term