Namdak Tonpa 5HT

Adapted to gist from https://unix.stackexchange.com/questions/344225/how-to-install-linux-on-the-playstation-2
Credits to Alison E.E.

Preambule

Looking to learn about game development? Are you a Linux enthusiast looking to test the claim that "Linux runs on everything"? Perhaps you are a software developer who is looking to release for multiple architectures, and you don't have another MIPS Little Endian machine on-hand for testing your programme. Whatever your situation there are a surprising number of reasons to install Linux on a Playstation 2, even sixteen years after it's release (boy do I feel old all of a sudden.), yet an equally surprising lack of documentation about it or how to install it.

Now don't get me wrong, if you want to use the original Sony Linux Kit, or one of it's updated open source releases on a fat PS2 with a network adapter and an IDE hard disk you can find plenty of info. However th

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

👋 Hi, I'm Geoff. I stole off all your NFTs.

I respectfully ask that you don't quote me as “$company person Geoffrey Huntley said” – if I speak for a company, I will publish on its channels. My full name is "Geoffrey Huntley" please use that and not "Geoff Huntley".

website: https://ghuntley.com/
newsletter: https://ghuntley.com/newsletter
twitter: https://www.twitter.com/geoffreyhuntley.com
linkedin: https://www.linkedin.com/in/geoffreyhuntley

No, your cryptocurrency cannot work

Whenever the topic of Bitcoin's energy usage comes up, there's always a flood of hastily-constructed comments by people claiming that their favourite cryptocurrency isn't like Bitcoin, that their favourite cryptocurrency is energy-efficient and scalable and whatnot.

They're wrong, and are quite possibly trying to scam you. Let's look at why.

What is a cryptocurrency anyway?

There are plenty of intricate and complex articles trying to convince you that cryptocurrencies are the future. They usually heavily use jargon and vague terms, make vague promises, and generally give you a sense that there must be something there, but you always come away from them more confused than you were before.

I'm writing this post to publicly come out as trans (specifically: I wish to transition to become a woman).

This post won't be as polished or edited as my usual posts, because that's kind of the point: I'm tired of having to edit myself to make myself acceptable to others.

I'm a bit scared to let people know that I'm trans, especially because I'm not yet in a position where I can transition (for reasons I don't want to share, at least not in public) and it's really shameful. However, I'm getting really

	global deps:
	- qmake
	- gcc
	- nodev14 + grunt
	- python2

	```
	$> npm instal -g grunt http-server

	#build for required deps (unknown for me) according to https://helpcenter.onlyoffice.com/ru/installation/docs-community-install-docker.aspx

	#include "liscpp.h"

	using namespace std;

	int main()
	{
	ReadEvalPrint(

	(Let,
	tok(fold), (Lambda, tok(F), tok(I), tok(L),

	open import Data.Nat
	open import Data.Maybe
	open import Data.Product

	-- An implementation of infinite queues fashioned after the von Neuman ordinals

	module Queue where

	infixl 5 _⊕_

	{-# OPTIONS --cubical #-}
	module Experiments where

	open import Agda.Builtin.Cubical.Path public
	open import Agda.Builtin.Cubical.Sub public renaming (primSubOut to ouc)
	open import Agda.Primitive.Cubical public
	renaming ( primIMin to _∧_ -- I → I → I
	; primIMax to _∨_ -- I → I → I
	; primINeg to -_ -- I → I
	; isOneEmpty to empty

	type expr =
	\| EVar of string
	\| EApp of expr * expr
	\| EPi of string * expr * expr
	\| ESig of string * expr * expr
	\| ELam of string * expr * expr
	\| EPair of expr * expr
	\| EFst of expr
	\| ESnd of expr
	\| ESet of int