Skip to content

Instantly share code, notes, and snippets.

View EduardoRFS's full-sized avatar
♥️
Laughing at the abysm

Eduardo Rafael EduardoRFS

♥️
Laughing at the abysm
982 followers · 114 following
View GitHub Profile
@EduardoRFS
EduardoRFS / controlled_fix.md
Created June 25, 2023 23:56 
Γ, x : %self(x). T |- T : Type
------------------------------
%self(x). T : Type

Γ, x : %self(x). T,
  eq : %self(eq). (P : T -> Type) -> P (%unroll x) -> P M |- M : T[x := M]
--------------------------------------------------------------------------
%fix(self%x : T, eq). M : %self(x). T
@EduardoRFS
EduardoRFS / bronen.ts
Created March 28, 2023 23:39
// EXAMPLE: (1 (2 3 *) +)
// ((1 (2 3 +) +) 4 +)
const exhaustive = <A>(x: never): A => x;
// interpreter
type Expression =
| { tag: "literal"; value: number }
| { tag: "operation"; operation: Operation };
@EduardoRFS
EduardoRFS / not_meaningful.md
Created March 11, 2023 18:21 
const flatArgsCore = (a, b) => a + b;
const objArgsCore = ({ a, b }) => a + b;
const size = 1e6;
const dataA = new Array(1e6).fill(0).map((_) => Math.random());
const dataB = new Array(1e6).fill(0).map((_) => Math.random());

const flatArgsAcc = () => {
  let acc = 0;
  for (let i = 0; i < 1e5; i++) {
@EduardoRFS
EduardoRFS / macabas.ts
Created March 10, 2023 17:29
const f = <
A extends "number" | "string",
T extends A extends "number" ? number : A extends "string" ? string : never
>(
_: A,
x: T
) => x;
const a = f("number", 1);
const b = f("string", "b");
@EduardoRFS
EduardoRFS / torrens.md
Created March 7, 2023 20:35 
((Bool,
  true : Bool,
  false : Bool,
  case : (b : Bool) -> (A : Type) -> A -> A -> A
) => M)(
  (A : Type) -> A -> A -> A,
  A => x => y => x,
  A => x => y => y,
 b =&gt; A =&gt; x =&gt; y =&gt; b A x y
@EduardoRFS
EduardoRFS / kewerson_self.md
Created March 2, 2023 16:07 
Γ, x : %self(x). T |- T : Type
------------------------------
%self(x). T : Type

fix%Unit (unit : %self(unit). %unroll Unit unit unit) (u : %self(u). %unroll Unit unit u)
  = (P : (u : %self(u). %unroll Unit unit u) -> Type) -> P unit -> P u;
fix%unit : %unroll Unit unit unit = P => x => x;

Unit = %self(u). %unroll Unit unit u;
@EduardoRFS
EduardoRFS / linf.v
Created February 2, 2023 17:08
From Coq Require Import Strings.String.
From Coq Require Logic.FunctionalExtensionality.
Inductive ty : Type :=
| T_Bool : ty
| T_Arrow : ty -> ty -> ty.
Inductive expr : Type :=
| E_var : string -> expr
| E_app : expr -> expr -> expr
| E_abs : string -> ty -> expr -> expr
@EduardoRFS
EduardoRFS / como_pensar.md
Created January 22, 2023 22:59

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

@EduardoRFS
EduardoRFS / stratified_induction.md
Last active February 9, 2023 22:06 
Set Universe Polymorphism.

Definition Eq_0 {A : Type} (x y : A) := forall (P : A -> Type), P x -> P y.
Definition refl_0 {A : Type} {x : A} : Eq_0 x x := fun P p_x => p_x.

Definition Eq_1 {T_0 : Type} {T_1 : T_0 -> Type} {x_0 y_0 : T_0} (x_1 : T_1 x_0) (y_1 : T_1 y_0)
  := forall (P : forall z_0, T_1 z_0 -> Type), P x_0 x_1 -> P y_0 y_1.
Definition refl_1 {T_0 : Type} {T_1 : T_0 -> Type} {x_0 : T_0} {x_1 : T_1 x_0} : Eq_1 x_1 x_1 := fun P p_x => p_x.
@EduardoRFS
EduardoRFS / weak_self_types.md
Created December 14, 2022 17:38 
// computing
C_bool = (A : Type) -> A -> A -> A;
(c_true : C_bool) = A => t => f => t;
(c_false : C_bool) = A => t => f => f;

// induction
I_bool b = (P : C_bool -> Type) -> P c_true -> P c_false -> P b;
i_true : I_bool c_true = P => p_t => p_f => p_t;
i_false : I_bool c_false = P => p_t => p_f => p_f;