cppio

opaque f : Nat → Nat
opaque g : Nat → Nat → Nat

inductive T : Nat → Type
  | mk₁ x : T (f x)
  | mk₂ x y : T (g x y)

theorem hcongrArg₂ {α : Sort u} {β : α → Sort v} {γ : ∀ a, β a → Sort w} (f : ∀ a b, γ a b) {a₁ a₂ : α} (ha : a₁ = a₂) {b₁ : β a₁} {b₂ : β a₂} (hb : HEq b₁ b₂) : HEq (f a₁ b₁) (f a₂ b₂) :=
  by cases ha; cases hb; rfl

cppio

inductive Le (x : Nat) : (y : Nat) → Prop
  | refl : Le x x
  | step : Le x y → Le x y.succ

inductive Ge (x : Nat) : (y : Nat) → Prop
  | refl : Ge x x
  | step : Ge x y.succ → Ge x y

inductive Le' : (x y : Nat) → Prop
  | zero : Le' .zero y

cppio

import Lean.Elab.Command

elab tk:"#show " "macro " i:ident : command => do
  let key ← Lean.Elab.Command.liftCoreM do Lean.Elab.realizeGlobalConstNoOverloadWithInfo i
  let env ← Lean.getEnv
  let names := Lean.Elab.macroAttribute.getEntries env key |>.map (·.declName)
  Lean.logInfoAt tk (.joinSep names Lean.Format.line)

elab tk:"#show " "term_elab " i:ident : command => do
  let key ← Lean.Elab.Command.liftCoreM do Lean.Elab.realizeGlobalConstNoOverloadWithInfo i

cppio

from collections import namedtuple

colors = namedtuple("colors", "black red green yellow blue magenta cyan white default")(0, 1, 2, 3, 4, 5, 6, 7, 9)
brightcolors = namedtuple("brightcolors", "black red green yellow blue magenta cyan white")(60, 61, 62, 63, 64, 65, 66, 67)
color = namedtuple("color", "r g b")
del namedtuple

def ansi(*, bold=None, underlined=None, inverse=None, foreground=None, background=None):
    params = []
    if bold is not None:

cppio

␀␁␂␃␄␅␆␇␈␉␊␋␌␍␎␏␐␑␒␓␔␕␖␗␘␙␚␛␜␝␞␟
␠!"#$%&'()*+,-./0123456789:;<=>?
@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_
`abcdefghijklmnopqrstuvwxyz{|}~␡

cppio

def foo : x = y → Bool := Eq.rec true
theorem bar : False = PEmpty := propext ⟨False.elim, PEmpty.elim⟩
theorem baz : Quot.mk (fun _ _ => True) false = Quot.mk _ true := Quot.sound trivial
theorem qux : foo h = true := h.rec (motive := fun _ h => h.rec true = true) rfl

example : foo bar = true := rfl
example : foo baz = true := rfl
example : foo bar = true := qux
example : foo baz = true := qux

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 => ⟨g, rfl, p⟩, fun ⟨_, p, q⟩ => inj p ▸ q⟩⟩

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))