damienstanton

extends Node2D

"""
c/o @martijnfolmer.bsky.social
source: https://github.com/martijnfolmer/Folmer_godot_samples

Small sample of what it looks like to simulate lines and cloth using verlet integration,
using 2 classes located in scripts/classes/class_verlet_cloth and /class_verlet_line.

Note that if you want to make it interact with the rest of the game, you would need

damienstanton

fn gcd1(mut m: i32, mut n: i32) -> i32 {
    let mut t = 0;
    while n != 0 {
        t = n;
        n = m % n;
        m = t;
    }
    m
}

damienstanton

structure Box α where
  val: α

namespace Box

def extract (b : Box α) := b.val

end Box

def a := Box.mk 42

damienstanton

Type theory (Thorsten Altenkirch)

Functions

Unlike in set theory, functions in type theory are by definition computable.

open import Data.Nat

f : ℕ → ℕ

damienstanton

# ╔════╗
# ║ DS ║
# ╚════╝
# version: 2025.07

# section: config
eval "$(/opt/homebrew/bin/brew shellenv)"
COMPLETION_WAITING_DOTS="true"
KEYTIMEOUT=1
plugins=(git

damienstanton

(ns user
  (:import (java.util.concurrent Executors)))

;; Thread factory for virtual threads
(defn thread-factory [name]
  (-> (Thread/ofVirtual)
    (.name name 0)
    (.factory)))

;; Define an executor which just produce a new virtual thread for every task

damienstanton

// This file implements a deep embedding of a typed-DSL in Go. The
// representation is type-safe (we cannot construct ill-typed terms)
// and accepts multiple interpretations. The type system of the target
// language is identity-mapped to the Go type system such that type
// checking of the DSL is hoisted up to type-checking the Go code that
// contains the target language expression.
//
// Normally this requires either GADTs or higher-rank types. I show
// that it is possible to encode it in Go, a language which doesn't
// have GADTs (nor regular ADTs for that matter), nor higher-rank

damienstanton

{
	"diagnostic.virtualText": true,
	"diagnostic.errorSign": "💣",
	"diagnostic.warningSign": "🚧 ",
	"diagnostic.infoSign": "📘 ",
	"diagnostic.hintSign": "🔎 ",
  	"python.linting.mypyEnabled": true,
	"haskell.liquidOn": true,
	"languageserver": {
		"go": {

damienstanton

I := λx.x

✅  I tweet = tweet
✅  I chirp = chirp
✅  I I = I

Idiot := I


Mockingbird := M := ω := λf.ff

damienstanton

// Either is an example of a sum type.
enum Either<Left, Right>
{
    Ok(Right),
    Err(Left)
}

// Point is an example of a product type.
type Point = (i64, i64, String);