EduardoRFS

type var = int

type term =
  (* x *)
  | T_var of var
  (* M N *)
  | T_apply of term * term
  (* x => M *)
  | T_lambda of var * term

EduardoRFS

N4 =
  | O
  | S
  | mod4 : Z == S(S(S(S(Z))));

B_N4 = (l : Bool, r : Bool);

in : _;

EduardoRFS

Definition Eq {A} (x y : A) := forall (P : A -> Type), P x -> P y.
Definition refl {A} {x : A} : Eq x x := fun P p_x => p_x.
Definition symm {A} {x y : A} (H : Eq x y) : Eq y x :=
  fun P p_y => H (fun z => P z -> P x) (fun x => x) p_y.

Lemma L_must_be_true (
  L_is_false : forall {T} {x y : T} (H : Eq x y),
    Eq H (fun P => symm H (fun z => P z -> P y) (fun x => x)) -> False
  ) : False.
  exact (L_is_false _ I I refl refl).

EduardoRFS

type term =
  | APP of term * term
  | VAR of var
  | FST of dup
  | SND of dup
  | SUP of term * term
  | LAM of var * term
  | NIL

and var = { mutable var : term }

EduardoRFS

// Post: https://x.com/VictorTaelin/status/1854326873590792276
// Note: The atomics must be kept.
// Note: This will segfault on non-Apple devices due to upfront mallocs.

#include <stdint.h>
#include <stdatomic.h>
#include <stdlib.h>
#include <stdio.h>
#include <time.h>

EduardoRFS

(* follow me on https://twitter.com/TheEduardoRFS *)

module Existentials = struct
  (* packed *)

  type show = Ex_show : { content : 'a; show : 'a -> string } -> show

  let value = Ex_show { content = 1; show = Int.to_string }

  let eval_show ex =

EduardoRFS

Set Universe Polymorphism.
Set Definitional UIP.

Inductive eqP (A : Type) (x : A) : A -> SProp :=
  | eqP_refl : eqP A x x.

Definition C_Bool : Type := forall A, A -> A -> A.
Definition c_true : C_Bool := fun A x y => x.
Definition c_false : C_Bool := fun A x y => y.

EduardoRFS

{-# OPTIONS --guardedness #-}

module stuff where

open import Agda.Builtin.Equality

symm : ∀ {l} {A : Set l} {n m : A} → n ≡ m → m ≡ n
symm refl = refl

record Pack {l} (A : Set l) (fst : A → A) : Set l where

EduardoRFS

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

EduardoRFS

title	date	tags
Reversing normalization for errors	2024-08-02 13:00:00 -0700	errors rewriting theory

Normalization is a technique used to ensure that any two objects that represent the same thing have the same form aka the normal form, a unique form of an expression.