Skip to content

Instantly share code, notes, and snippets.

View wrongbyte's full-sized avatar
🍊
I like orange juice

wrongbyte

🍊
I like orange juice
View GitHub Profile
Definition sig_fst {A B} {p q : {x : A | B x}} (H : p = q)
: proj1_sig p = proj1_sig q :=
eq_rect _ (fun z => proj1_sig p = proj1_sig z) eq_refl _ H.
Definition sig_snd {A B} {p q : {x : A | B x}} (H : p = q)
: eq_rect _ B (proj2_sig p) _ (sig_fst H) = proj2_sig q :=
match H with
| eq_refl => eq_refl
end.
@leo-aa88
leo-aa88 / bluetoothctl_guide.md
Created January 12, 2025 01:59
bluetoothctl guide

Guide to Connecting to a Bluetooth Device using bluetoothctl

This guide walks you through the process of connecting to a Bluetooth device on a Linux system using the bluetoothctl command-line tool. It covers initial setup, scanning, pairing, and connecting procedures, along with troubleshooting tips.

Prerequisites

  • A Linux distribution with Bluetooth support (e.g., Arch Linux).
  • The bluez package installed, which provides bluetoothctl and related utilities.
  • A working Bluetooth adapter installed on your system.
  • Sudo privileges to execute commands that require root access.
type never = |
type ('a, 'b) equal = Refl : ('x, 'x) equal
type ('l, 'r) dec_equal =
| D_refl : ('l, 'l) dec_equal
| D_neq : (('l, 'r) equal -> never) -> ('l, 'r) dec_equal
let ( let* ) v f = Option.bind v f
module Nat = struct
@quad
quad / 0-modular-errors-with-rusts-thiserror.md
Last active October 31, 2025 19:58
Modular Errors with Rust's thiserror

I've been writing Rust full-time with a small team for over a year now. Throughout, I've lamented the lack of clear best practices around defining error types. One day, I'd love to write up my journey and enumerate the various strategies I've both seen and tried. Today is not that day.

Today, I want to reply to a blog post that almost perfectly summarised my current practice.

Go read it; I'll wait!


Como Pensar

Ler e entender um pouco desse artigo. https://wiki.c2.com/?FeynmanAlgorithm

  • Reconhecer como você pensa
  • Descrever métodos que você usa para pensar
  • Entender métodos diferentes de pensar
  • Fazer perguntas sobre tudo(incluindo sobre perguntas)

Perguntas

@algebraic-dev
algebraic-dev / tt.rs
Last active February 12, 2024 22:34
Dependent type checker with substitution for lambda calculus.
use std::{collections::HashSet, fmt::Display, rc::Rc};
/// The AST. This thing describes
/// the syntatic tree of the program.
#[derive(Debug)]
pub enum Syntax {
Lambda {
param: String,
body: Rc<Syntax>,
},

Roadmap de estudos de SQL

Aviso: Muitas vezes detalhes de várias operações podem variar de banco para banco. Em questões onde fiquei em dúvida, este documento segue o funcionamento do PostgreSQL, pois é o banco que conheço melhor.

Pré-requisito: Álgebra Relacional básica

Antes de começar a escrever SQL, você precisa entender o modelo de como um banco de dados relacional funciona. Não precisa se aprofundar muito, mas você precisa entender como que dados e relacionamentos entre eles são representados. (Nota importante: Relacionamento e relação não são a

@pranavdeshai
pranavdeshai / nord.json
Last active March 4, 2025 20:04
Nord theme for Anki UI using the ReColor add-on
{
"colors": {
"BORDER": [
"Border",
"#D8DEE9",
"#434C5E",
"--border"
],
"BURIED_FG": [
"Buried Foreground",