cppio

import dis, sys

def varnames():
    frame = sys._getframe(1)
    instrs = dis.get_instructions(frame.f_code)
    instr = next(instr for instr in instrs if instr.offset > frame.f_lasti)
    match instr.opname:
        case "STORE_FAST" | "STORE_GLOBAL" | "STORE_NAME":
            return instr.argval
        case "STORE_FAST_LOAD_FAST":

cppio

def sig(fn):
    code = fn.__code__
    defaults = fn.__defaults__
    kwdefaults = fn.__kwdefaults__
    if defaults is None:
        defaults = ()
    if kwdefaults is None:
        kwdefaults = {}

    pos, varnames = code.co_varnames[:code.co_argcount], code.co_varnames[code.co_argcount:]

cppio

import types

class StaticMethod:
    def __init__(self, f):
        self.f = f

    def __get__(self, instance, owner):
        return self.f

class ClassMethod:

cppio

╭───────╮
│ Hello │
╰───────╯

┌───────┐
│ Hello │
└───────┘

┏━━━━━━━┓
┃ Hello ┃

cppio

import Lean.Elab.Term

deriving instance Lean.ToExpr for String.Pos
deriving instance Lean.ToExpr for Substring
deriving instance Lean.ToExpr for Lean.SourceInfo
deriving instance Lean.ToExpr for Lean.Syntax

syntax "log! " (interpolatedStr(term) <|> term:arg) : term

@[term_elab termLog!__]

cppio

-- https://arxiv.org/abs/1911.08174
def T : Prop := ∀ p, (p → p) → p → p
def δ (z : T) : T := fun p η h => η (z (T → T) id id z p η h)
def ω : T := fun _ _ h => propext ⟨fun _ => h, fun _ => id⟩ ▸ δ
def Ω : T := δ ω

noncomputable def WellFounded.fix' {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Sort v} (F : ∀ x, (∀ y, r y x → C y) → C x) x : C x :=
  @Acc.rec α r (fun x _ => C x) (fun x _ => F x) x (Ω (∀ x, Acc r x) (fun wf x => ⟨x, fun y _ => wf y⟩) hwf.apply x)

theorem WellFounded.fix'_eq : @WellFounded.fix' α r hwf C F x = F x fun y _ => hwf.fix' F y := rfl

cppio

noncomputable def inf : Acc (fun _ _ => True) () → Nat := Acc.rec fun _ _ ih => ih () ⟨⟩ + 1

example : inf h = inf h + 1 := @id (inf h = inf ⟨_, fun _ _ => h⟩) rfl
-- example : inf h = inf h + 1 := rfl -- fails

-- https://arxiv.org/abs/1911.08174
def T : Prop := ∀ p, (p → p) → p → p
def δ (z : T) : T := fun p η h => η (z (T → T) id id z p η h)
def ω : T := fun _ _ h => propext ⟨fun _ => h, fun _ => id⟩ ▸ δ
def Ω : T := δ ω

cppio

{-# OPTIONS --rewriting --confluence-check #-}

module Hurkens where

open import Agda.Builtin.Equality
import Agda.Builtin.Equality.Rewrite

postulate
  Π₁ : (Set₁ → Set₁) → Set₁
  λ₁ : ∀ {F} → (∀ A → F A) → Π₁ F

cppio

inductive Tree : Sort (max (u + 1) v)
  | node {A : Sort u} (c : A → Tree)

theorem no_embedding
  (Lower : Sort (max (u + 1) v) → Sort u)
  (down : ∀ {α}, α → Lower α)
  (up : ∀ {α}, Lower α → α)
  (up_down : ∀ {α} (x : α), x = up (down x))
: False := by
  induction h : Tree.node up

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