forked-from-1kasper

universe u

inductive Eq' {A : Type u} : A → A → Type u
| idp (a : A) : Eq' a a

def f {A : Type u} {a b : A} : Eq' a b → Eq a b :=
λ q => @Eq'.casesOn A a (λ b q' => Eq a b) b q (Eq.refl a)

def g {A : Type u} {a b : A} : Eq a b → Eq' a b :=
λ p => @Eq.casesOn A a (λ b p' => Eq' a b) b p (Eq'.idp a)

forked-from-1kasper

#! /usr/bin/bash

# $ echo -n Π U Z Π 0 Π 1 U Z > Id
# $ ./dtt.sh λ U Z λ 0 λ 1 β β β Id 2 1 0
# INFER: Π U Z Π 0 Π 1 U Z
# EVAL: λ U Z λ 0 λ 1 β β β Id 2 1 0

function head() {
    echo $* | cut -d" " -f1
}

forked-from-1kasper

import Lean.Elab.Command
open Lean

elab "#defeq " σ₁:term " =?= " σ₂:term : command =>
  Elab.Command.liftTermElabM (do
    let τ₁ ← Elab.Term.elabTerm σ₁ none
    let τ₂ ← Elab.Term.elabTerm σ₂ none
    unless (← Meta.isDefEq τ₁ τ₂) do throwError s!"{τ₁} ≠ {τ₂}")

#defeq [1, 2, 3, 4].reverse =?= [4, 3, 2, 1]

forked-from-1kasper

noncomputable section
namespace MWE

universe u v w

inductive Id {A : Type u} : A → A → Type u
| refl {a : A} : Id a a

attribute [eliminator] Id.casesOn

forked-from-1kasper

module patt where

data nat
  = zero
  | succ (n : nat)

natToZero : nat -> nat = split
  zero ha ha ha -> zero
  succ cubicaltt is a w e s o m e -> zero

forked-from-1kasper

import Lean.Meta.Reduce
import Lean.Parser.Term
import Lean.Expr
import Lean.Elab
open Lean

axiom I  : Type
axiom i₀ : I
axiom i₁ : I

forked-from-1kasper

from dataclasses import dataclass
from random import random

@dataclass
class Vector:
    x : float
    y : float

    def __sub__(v1, v2):
        return Vector(v1.x - v2.x, v1.y - v2.y)

forked-from-1kasper

Good afternoon!

I’d like to tell you about a major case of violation by the person with the nickname @5HT.

He hired me for type theory research and I worked successfully from 2018 to 2022 until February 28 he decided to break any relationship with me and kicked me out of the Groupoid organization where my projects were located.

A few days later, all my commits in that organization were no longer connected to my account.

@5HT said that this caused by ban in organization, but, very strangely, @forked-from-1kasper disappeared in contributors statistics

forked-from-1kasper

module inv where

Path (A : U) (a b : A) : U = PathP (<_> A) a b

inv1 (A : U) (a b : A) (p : Path A a b) : Path A b a =
  <i> p @ -i

inv2 (A : U) (a b : A) (p : Path A a b) : Path A b a =
  <i> comp (<_> A) a [(i = 0) -> p, (i = 1) -> <_> a]

forked-from-1kasper

type path =
  | Var of string
  | Ref
  | Trans of path * path
  | Rev of path

let rec show : path -> string = function
  | Var x -> x
  | Ref -> "ref"
  | Trans (p, q) -> Printf.sprintf "(%s * %s)" (show p) (show q)