Skip to content

Instantly share code, notes, and snippets.

🌚
donos

Andrew / Kana kana-sama

🌚
donos
Block or report user

Report or block kana-sama

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View set_theory.idr
module Main
infix 5 /\, \/
(/\) : Type -> Type -> Type
(/\) a b = (a, b)
(\/) : Type -> Type -> Type
(\/) a b = Either a b
View 2.11.thy
datatype exp = Var | Const int | Add exp exp | Mult exp exp
fun eval where
"eval Var v = v" |
"eval (Const x) v = x" |
"eval (Add a b) v = eval a v + eval b v" |
"eval (Mult a b) v = eval a v * eval b v"
fun evalp :: "int list ⇒ int ⇒ int" where
"evalp [] v = 0" |
View sqrt_2_irrat.lean
reserve postfix `²`:std.prec.max_plus
notation x² := x^2
namespace nat
namespace parity
def even (n : ℕ) := n%2 = 0
def odd (n : ℕ) := ¬even n
lemma even_of_dvd {n} : 2∣n → even n :=
mod_eq_zero_of_dvd
View group.lean
namespace hidden
class group (α : Type) extends has_mul α, has_one α, has_inv α :=
(mul_assoc : ∀(a b c : α), (a * b) * c = a * (b * c))
(e_mul : ∀(x : α), 1 * x = x)
(mul_e : ∀(x : α), x * 1 = x)
(mul_right_inv : ∀(x : α), x * x⁻¹ = 1)
namespace group
variables {α : Type} [group α]
View groups.lean
namespace hidden
structure group :=
(α : Type)
(mul : α → α → α)
(e : α)
(inv : α → α)
(mul_assoc : ∀a b c : α, mul (mul a b) c = mul a (mul b c))
(e_mul : ∀x, mul e x = x)
(mul_e : ∀x, mul x e = x)
View nat_parity.lean
inductive vector (α : Type) : ℕ → Type
| nil {} : vector 0
| cons {n : ℕ} : α → vector n → vector (nat.succ n)
def x := vector.cons "1" (vector.cons "2" (vector.cons "3" vector.nil))
#check x
#check (⟨3, x⟩ : Σn, vector string n)
#check nat.le_refl
#check nat.le_refl 10
View curry.ts
type List = readonly any[];
type cons<x, xs extends List> = ((x: x, ...xs: xs) => any) extends ((
...ys: infer ys
) => any)
? ys
: never;
type uncons<ys extends List> = ((...ys: ys) => any) extends ((
x: infer x,
View example.ts
import { observable, action, computed, flow } from "mobx";
import { IHTTP } from "./http/interface";
import { ConversationsItem } from "../types";
class RemoteData<T> {
@observable public isLoaded: boolean = false;
@observable public isLoading: boolean = false;
@observable public isFailed: boolean = false;
@observable public dataValue: T | null = null;
View qwe.js
import * as React from "react";
import * as ReactDOM from "react-dom";
import { observable, action } from "mobx";
import { useLocalStore, useObserver } from "mobx-react-lite";
class CurrentUserModel {
@observable value = null;
@action fetch() {
setTimeout(() => {
View qwe.js
class Users {
constructor(http) {
this.http = http;
this.cache = new Map();
}
get(id, next) {
if (this.cache.has(id)) {
next(this.cache.get(id));
}
You can’t perform that action at this time.