Peng Cheng tribbloid

🌴

differentiable - functional - axiomatic

tribbloid / gist:19e4fab8ec7bcd5acfe7a1cfccce843a

Created May 22, 2026 19:24

Lean4 transport hell demo


	set_option synthInstance.checkSynthOrder false


	inductive Vec : Nat -> Type
	\| mk (n: Nat) (data: List Nat) : Vec n
	deriving DecidableEq

	instance vecTransport {x y : Nat} {ev: x = y} : Coe (Vec x) (Vec y) where
	coe v := cast (congrArg Vec ev) v

tribbloid / scaffold.lean

Last active May 19, 2026 19:31

A short demo on how to use PHOAS & Fixed-point bound conjecture to write short evaluation and compilation rules


	namespace DTLC
	/-
	dependently typed lambda calculus (similar to STLC but function output type can depend on input term) with a top/wildcard type.

	chosen as a nerfed System D (as in "The Essence of Dependent Object Types") for some sanity/vibe check.
	-/

	abbrev Index := Type -- AKA symbol, PHOAS carrier
	def ByteCode := String

tribbloid / gist:b8c27b98299f473f4461636010266553

Last active April 6, 2025 19:18

Scala effect-zoo benchmark (04/03/2025 master)

	/opt/homebrew/Cellar/openjdk/23.0.2/libexec/openjdk.jdk/Contents/Home/bin/java -server -Xmx1536M -Dsbt.supershell=false -Djdk.console=java.base -Dgrouping.with.qualified.names.enabled=true -Dseparate.prod.test.sources.enabled=false -Didea.managed=true -Dfile.encoding=UTF-8 "-Didea.installation.dir=/Users/pengcheng/Applications/IntelliJ IDEA Community Edition.app/Contents" -Dsun.stdout.encoding=UTF-8 -Dsun.stderr.encoding=UTF-8 -jar "/Users/pengcheng/Library/Application Support/JetBrains/IdeaIC2024.3/plugins/Scala/launcher/sbt-launch.jar" early(addPluginSbtFile=\"\"\"/private/var/folders/fy/9k8fbqlx1fb4ndlvfhv5r3ph0000gn/T/idea.sbt\"\"\") idea-shell
	[info] welcome to sbt 1.9.0 (Homebrew Java 23.0.2)
	[info] loading settings for project effect-zoo-build-build-build from metals.sbt ...
	[info] loading project definition from /Users/pengcheng/git-release/effect-zoo/project/project/project
	[info] loading settings for project effect-zoo-build-build from metals.sbt ...
	[info] loading project definition from /Users/pen

tribbloid / AutoLift.scala

Created February 22, 2024 02:28

SerializingAutoLift & TypeTag in 100 lines, for Scala 3

	import java.io.{ByteArrayInputStream, ByteArrayOutputStream, ObjectInputStream, ObjectOutputStream}
	import java.util.Base64
	import scala.quoted.*

	object AutoLift {
	trait SerializingAutoLift[T] extends ToExpr[T] {

	def apply(x: T)(
	using
	Quotes

tribbloid / questions.ipynb

Last active April 21, 2018 23:23

2 questions for rigid body dynamics.

Sorry, something went wrong. Reload?

Sorry, we cannot display this file.

Sorry, this file is invalid so it cannot be displayed.

tribbloid / JCETester.scala

Created January 17, 2018 02:56

Scala JCE Strength tester

	import javax.crypto.Cipher;

	val maxKeyLen = Cipher.getMaxAllowedKeyLength("AES")
	println(maxKeyLen)

tribbloid / test.py

Created December 22, 2016 18:16

MAVProxy/Dronekit-python integration test on waypoint download

	import dronekit
	import pexpect
	import sys
	import time
	from dronekit_sitl import SITL

	sys.path.append('/home/peng/.spookystuff/pythonpath')
	import os

	sitl_args = ['--model', 'quad', '--home=-35.363261,149.165230,584,353']

tribbloid / dronekit-mavproxy-test.py

Created December 22, 2016 17:53

Usually commands.download() will fail after 4-6 trials. It won't happen without MAVProxy

	import dronekit
	import pexpect
	import sys
	import time
	from dronekit_sitl import SITL

	sys.path.append('/home/peng/.spookystuff/pythonpath')
	import os

	sitl_args = ['--model', 'quad', '--home=-35.363261,149.165230,584,353']

tribbloid / running gradle build on dronekit-android

Created June 29, 2016 23:34

	:init
	The build file 'build.gradle' already exists. Skipping build initialization.
	:init SKIPPED

	BUILD SUCCESSFUL

	Total time: 8.814 secs

	This build could be faster, please consider using the Gradle Daemon: https://docs.gradle.org/2.14/userguide/gradle_daemon.html
	peng@peng-tribbloids:~/git-drone/dronekit-android$