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
984 followers · 114 following
View GitHub Profile
@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 / 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 / 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 / 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;
@EduardoRFS
EduardoRFS / iup_induction.md
Last active December 8, 2022 00:08 
// Church booleans
C_bool : Type 1 = (L : Level) -> (A : Type L) -> A -> A -> A;
c_true : Bool = L => A => t => f => t;
c_false : Bool = L => A => t => f => f;

// Induction principle
I_bool = b : Type 1 => (L : Level) -> (P : C_bool -> Type L) -> P c_true -> P c_false -> P b;
// Without IUP, Bool would be placed on Type Omega, making it useless
Bool : Type 1 = (b : Bool) &amp; (ind : I_bool b);
@EduardoRFS
EduardoRFS / settings.json
Created September 12, 2019 17:24
VSCode settings
{
// fonts
"editor.fontSize": 18,
"markdown.preview.fontSize": 18,
"terminal.integrated.fontSize": 18,
"editor.fontLigatures": true,
"editor.fontFamily": "'Fira Code'",
"terminal.integrated.fontFamily": "Consolas, 'Fira Code'",
"workbench.iconTheme": "material-icon-theme",
@EduardoRFS
EduardoRFS / dependent_elimination.md
Last active December 1, 2022 20:59 
refl : {A} -> A == A = _;
C_bool = {A} -> A -> A -> A;
c_true : C_bool = {A} => t => f => t;
c_false : C_bool = {A} => t => f => f;

Ind_bool : C_bool -> Type =
  b => {P} -> P c_true -> P c_false -> P b;
ind_true : Ind_bool c_true = {P} => t => f => t;
ind_false : Ind_bool c_false = {P} => t => f => f;