CoderPuppy

module Komi20250302 where

data _≡_ {A : Set} (base : A) : A → Set where
  refl : base ≡ base

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl p = p

CoderPuppy

local FUEL_TARGET = 1024
local FILLER_TARGET = 128
local ignore_blocks = {
	['minecraft:stone'] = true;
	['minecraft:cobblestone'] = true;
	-- ['minecraft:andesite'] = true;
	-- ['minecraft:diorite'] = true;
	-- ['minecraft:granite'] = true;
	-- ['minecraft:dirt'] = true;
	['minecraft:deepslate'] = true;

CoderPuppy

set $HOME /home/cpup
set $GUIX $HOME/.guix-profile

output eDP-1 {
	mode 2880x1800@60Hz
	scale 1.5
	pos 1920 0
}

output "Hewlett Packard HP LP2475w CNC0510PV3" {

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