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
1.1k followers · 127 following
View GitHub Profile
@EduardoRFS
EduardoRFS / nat_by_j.v
Last active October 28, 2025 23:24
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.
@EduardoRFS
EduardoRFS / bool_by_j_cc.v
Last active October 24, 2025 16:55
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.
@EduardoRFS
EduardoRFS / coherence_either.v
Created October 23, 2025 19:23
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.
@EduardoRFS
EduardoRFS / bool_by_j_pred.v
Created October 22, 2025 03:18
Definition sig_fst {A B} {p q : {x : A & B x}} (H : p = q)
: projT1 p = projT1 q :=
eq_rect _ (fun z => projT1 p = projT1 z) eq_refl _ H.
Definition sig_snd {A B} {p q : {x : A & B x}} (H : p = q)
: eq_rect _ B (projT2 p) _ (sig_fst H) = projT2 q :=
match H with
| eq_refl => eq_refl
end.
@EduardoRFS
EduardoRFS / bool_by_j.v
Last active October 24, 2025 02:25
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.
@EduardoRFS
EduardoRFS / naive_vars.ml
Created October 1, 2025 22:04
type term = T_var of var | T_lambda of var * term | T_apply of term * term
and var = { mutable to_ : term }
let v_with var ~to_ k =
let prev = var.to_ in
var.to_ <- to_;
let value = k () in
var.to_ <- prev;
value
@EduardoRFS
EduardoRFS / lazy-optimal.ml
Last active September 22, 2025 21:08
type index = int
type term =
| T_var of index
| T_lambda of term lazy_t
| T_apply of term lazy_t * term lazy_t
let rec shift ~by ~depth term =
match term with
| T_var var -> (
@EduardoRFS
EduardoRFS / better-optimal.ml
Last active August 31, 2025 23:42
(*
Start with an environment based interpreter that does
all the reductions, including under lambdas.
Then make everything not on the head path lazy.
When you go to evaluate everything on the side,
you force the head producing a potentially stuck value
and then apply the new environment, progressing further.
Lazy act like graph sharing for every reduction on the side.
@EduardoRFS
EduardoRFS / simple-optimal.ml
Last active September 1, 2025 19:48
(*
Start with an environment based interpreter that does
all the reductions, including under lambdas.
Then make everything not on the head path lazy.
When you go to evaluate everything on the side,
you force the head producing a potentially stuck value
and then apply the new environment, progressing further.
Lazy acts like graph sharing for reductions on the side.
@EduardoRFS
EduardoRFS / nbe-optimal.ml
Last active August 16, 2025 21:42
(* this whole thing is a sketch *)
type var = int [@@deriving show { with_path = false }]
type term =
| T_var of var
| T_let of var * term * term
| T_lambda of var * term
| T_apply of term * term
| T_reify of thunk