Kha

import Aesop

variable [LE α] [DecidableRel ((· ≤ ·) : α → α → Prop)]

@[aesop safe constructors]
inductive Sorted : List α → Prop where
  | nil : Sorted []
  | single : Sorted [x]
  | cons_cons : x ≤ x' → Sorted (x' :: xs) → Sorted (x :: x' :: xs)

Kha

class Trans (r : α → β → Prop) (s : β → γ → Prop) (t : outParam (α → γ → Prop)) where
  trans : r a b → s b c → t a c

export Trans (trans)

instance (r : α → γ → Prop) : Trans Eq r r where
  trans heq h' := heq ▸ h'

instance (r : α → β → Prop) : Trans r Eq r where
  trans h' heq := heq ▸ h'

Kha

Kha

import data.set.finite

-- we don't need no infinite sets here
open finset
open function

-- `fin n` is the type of the first `n` natural numbers
theorem pigeonhole (n m : ℕ) (f : fin n → fin m) : n > m → ¬(injective f) :=
assume : n > m,
-- proof of negation: show contradiction

Kha

section
universe u
parameters (α β : Type u) (op : α → β → Prop)

structure chained_op_val :=
(left : α)
(right : β)
(val : Prop)

instance coe_chained_op_val : has_coe chained_op_val Prop :=

Kha

namespace nqueens
open nat

class lt (n : out_param ℕ) (m : ℕ)
instance succ_lt_succ_of_lt (n m) [lt n m] : lt (succ n) (succ m) := by constructor
instance zero_lt_succ (m) : lt 0 (succ m) := by constructor

class ne (n m : ℕ)
instance ne_of_lt (n m) [lt n m] : ne n m := by constructor
instance ne_of_gt (n m) [lt m n] : ne n m := by constructor

Kha

import data.int.basic
import data.int.order

open bool
open int
open eq.ops

-- 1

abbreviation Var := string

Kha

	public class MatchVariants : TowerFall.MatchVariants
	{
		public Variant NoHeadBounce;
	}

	public class Player : TowerFall.Player
	{
		public override void BouncedOn(TowerFall.Player bouncer)
		{
			if (!((MatchVariants)Level.Session.MatchSettings.Variants).NoHeadBounce)

Kha

import socket, json
import random, pprint
import sys
import math
import re

class arith_list(list):
    def __add__(self, other):
        return arith_list([x + y for x, y in zip(self, other)])

Kha

def heap_rec(f):
    stack = [f]
    result = None
    while stack:
        try:
            stack.append(stack[-1].send(result))
            result = None
        except StopIteration as ex:
            result = ex.value
            stack.pop()