Jason jcreedcmu

asynchronous frankenpigeon

A conlanging game for perhaps 3-5 players, suitable for a shared editable document.

All players edit a shared document.
At the top of the document is the "word bank": for each player, there is a list of between 0 and 5 words. For example, it might look like:

Alice	Bob	Carol

A conlanging game for perhaps 3-5 players, suitable for VC.

All players prepare a list of 5 made-up words, and decide on an ordering of the players.
Each player passes their word list to the next player in this order, wrapping around.
Players take turns.
On their turn, a player makes an utterance, and simultaneously tries to convey its meaning.
The utterance is in a made-up language that grows as the game goes on: the player can use words on their own list, plus any words they've already heard from other players. Using proper nouns (such as players' names) is always allowed.

This cost $5.43 This cost $3

This cost $5.43 This cost $

	import Mathlib

	class Grph (G : Type) where
	edge : G → G → Prop
	open Grph

	variable {G H : Type} [Grph G] [Grph H]

	structure Hom (G H : Type) [Grph G] [Grph H] where
	obj : G → H

	import Mathlib

	/--
	Do one collatz iteration
	-/
	def collatz (n : Nat) :=
	if n % 2 == 0 then n / 2 else 3 * n + 1

	/-
	Algorithmic collatz termination

	{-# OPTIONS --cubical #-}

	open import Cubical.Foundations.Prelude
	open import Cubical.HITs.S1

	module Braids1 where

	{-

	Conjecture:

	def foo : Nat := (1 + 2)
	def bar : Nat := (3 + 4)