cppio

def cantor_sur (f : α → (α → Prop)) : { g // ∀ x, g ≠ f x } :=
  ⟨fun x => ¬f x x, fun x h => not_iff_self <| iff_of_eq <| congrFun h x⟩

def cantor_inj (f : (α → Prop) → α) : { g // ¬(∀ {h}, f g = f h → g = h) } :=
  let g x := ∀ h, x = f h → ¬h x
  ⟨g, fun inj => @not_iff_self (g (f g)) ⟨fun p _ q => inj q ▸ p, fun p => p g rfl⟩⟩

namespace NonStrictlyPositiveInductive

unsafe inductive T

cppio

variable {α : Sort u} (r : α → α → Prop)

inductive EqvClos a : α → Prop
  | refl : EqvClos a a
  | step : r b c → EqvClos a b → EqvClos a c
  | unstep : r b c → EqvClos a c → EqvClos a b

variable {r}

def Quot.exact (h : mk r a = mk r b) : EqvClos r a b :=

cppio

inductive Fin2 : (n : Nat) → Type
  | zero : Fin2 (.succ n)
  | succ (i : Fin2 n) : Fin2 n.succ

def Fin2.elim0 {C : Fin2 .zero → Sort u} : ∀ i, C i := nofun

def Fin2.cases {C : Fin2 (.succ n) → Sort u} (zero : C .zero) (succ : ∀ i, C (.succ i)) : ∀ i, C i
  | .zero => zero
  | .succ i => succ i

cppio

fun addr x = Unsafe.Pointer.AddrWord.toLarge (Unsafe.Pointer.toWord (Unsafe.cast x))

cppio

theorem choice {α : Sort u} {β : α → Sort v} (h : ∀ x, Nonempty (β x)) : Nonempty (∀ x, β x) := ⟨fun x => Classical.choice (h x)⟩
theorem setext {α : Sort u} {A B : α → Prop} (h : ∀ x, A x ↔ B x) : A = B := funext fun x => propext (h x)

theorem em : P ∨ ¬ P :=
  let A x := P ∨ x = false
  let B x := P ∨ x = true
  let ⟨f⟩ := choice fun C : { C : Bool → _ // ∃ x, C x } => let ⟨x, h⟩ := C.property; ⟨Subtype.mk x h⟩
  let a := f ⟨A, false, .inr rfl⟩
  have (B) : (h : A = B) → a.val = (f ⟨B, false, h ▸ .inr rfl⟩).val
    | rfl => rfl

cppio

inductive Void : Prop
  | void (v : Void) : Void

/-
def inf : Void → Nat
  | .void v => .succ (inf v)
-/
noncomputable def inf : Void → Nat := @Void.rec _ fun _ => .succ

example (v : Void) : inf v = inf (.void v) := rfl

cppio

import Batteries.WF

abbrev ExistsAfter (P : Nat → Prop) := Acc fun y x => y = x.succ ∧ ¬P x

inductive Nat.ge (n : Nat) : Nat → Prop
  | refl : ge n n
  | step : ge n m.succ → ge n m

theorem Nat.ge_succ : ge n m → ge n.succ m
  | .refl   => .step .refl

cppio

use std::{
    mem::ManuallyDrop,
    ops::{Deref, DerefMut},
};

pub trait BoxDrop {
    fn drop(self: Box<Self>);
}

#[repr(transparent)]

cppio

#[repr(usize)]
pub enum Tree<T> {
    Leaf(T),
    Node(DropBox<Self>, DropBox<Self>),
}

impl<T> BoxDrop for Tree<T> {
    fn drop(self: Box<Self>) {
        #[repr(usize)]
        enum RawTree<T> {

cppio

docker run -it --rm alpine
# inside
apk add gdb-multiarch
wget https://gist.githubusercontent.com/cppio/6576572073a424b01b9d0c9a2e4bade5/raw/42aa93d2be602e343792a59587d7a8ad7152a7d8/hello.x86_64
chmod +x hello.x86_64
ROSETTA_DEBUGSERVER_PORT=12345 ./hello.x86_64 &
gdb-multiarch hello.x86_64 -ex 'tar rem :12345'