basic-calculus’s gists

basic-calculus / f32.c

Created January 11, 2023 18:52

Portable code for https://outerproduct.net/trivial/2023-01-11_nan.html GCC compiles this right

	#include <math.h>
	#include <stddef.h>
	#include <stdint.h>
	#include <stdio.h>
	#include <string.h>

	/* quiet NANs aren't always defined???
	confused about this bit
	*/
	#define F32 NAN

basic-calculus / search.org.githubdontstomponlinks

Last active December 18, 2022 06:12

Side by side with org mode. Something like this might work? It would be nice if you could use a more typical markup language like markdown though

	[[file:search.mjs::history.scrollRestoration]]

	FIXME unsure about scroll restoration.

	[[file:search.mjs::function clickRequest(]]

	Filter to non modifier, non chorded mouse clicks.

	[[file:search.mjs::function submitRequest(]]

basic-calculus / sidebyside.mjs

Last active December 18, 2022 05:36

I deal with ADHD and struggle to hold context together in my head. So code comments confuse me. Even code folding gets too confusing for me. I like the idea of seing comments side by side with source code but no editor really supports this? I've tried 2C in emacs in the past but it's kind of awkward and not really made for this.

	const pfimp = import('./pagefind/pagefind.js'); // Import pagefind

	history.scrollRestoration = 'manual'; // FIXME unsure about scroll restoration

	const { origin, pathname, searchParams } = new URL(location);

	function searchlink(p, x) {
	const params = new URLSearchParams({[p]: x});
	return `${pathname}?${params}`;
	}

basic-calculus / tree.v

Last active October 30, 2022 00:23

	Inductive sort := domain \| function (A B: sort).
	Inductive context:=
	\| nil
	\| one (A: sort)
	\| append (A B: context).

	Inductive Var (A: sort): context -> Set :=
	\| VO: Var A (one A)
	\| VL G D: Var A D -> Var A (append G D)
	\| VR G D: Var A G -> Var A (append G D).

basic-calculus / tagsareannoying.v

Last active October 28, 2022 01:33

	Require Import Coq.Unicode.Utf8.
	Require Import Coq.Strings.String.
	Require Coq.Vectors.Vector.
	Require Coq.Vectors.Fin.

	Import IfNotations.

	Set Primitive Projections.

basic-calculus / description.v

Last active October 27, 2022 17:35

Some extremely basic description stuff

	Require Import Coq.Unicode.Utf8.

	Import IfNotations.

	Inductive U: Set :=
	\| self
	\| void
	\| sum (A B: U)
	\| unit
	\| prod (A B: U).

basic-calculus / computable.v

Created October 26, 2022 02:00

Computable sets

	Require Import Coq.Unicode.Utf8.
	Require Coq.Program.Basics.

	Import IfNotations.

	Inductive SET := image (A: Set) (π: A → SET).

	Definition index (X: SET) :=
	let '(image A _) := X in A.
	Definition π (X: SET): index X → SET :=

basic-calculus / ring-and-the-cup-part-2-THE QUEST.txt

Created October 17, 2022 22:51

Excerpt from the ring and the cup, an epic poem I was working on a few years ago.

	war lost, Two was exiled and turned to banditry
	where he assailed souls from all sides

	till one day dreaming Two's heart rose up
	and sleeping in a cave he had a dream

	lift up, take up, stand up, young son, lost one, lost son

	go seek the ring - find the cup, rise up young son
	you live today - your heart beats still - and still sings on

basic-calculus / universe.v

Created October 16, 2022 22:55

	Require Import Coq.Unicode.Utf8.
	Require Coq.Program.Equality.
	Require Coq.Vectors.Vector.
	Require Coq.Lists.List.

	Import IfNotations.
	Import List.ListNotations.
	Import Vector.VectorNotations.

	Section SET.

basic-calculus / untyped.v

Last active October 13, 2022 22:53

Some basic untyped lambda calculus semantics

	Require Import Coq.Unicode.Utf8.
	Require Import Coq.Classes.RelationClasses.
	Require Import Coq.Classes.SetoidClass.
	Require Import Coq.Program.Basics.
	Require Import Coq.Relations.Relation_Definitions.
	Require Coq.Vectors.Vector.
	Require Coq.Vectors.Fin.
	Require Coq.Lists.List.

	Import IfNotations.

m basic-calculus