EduardoRFS

type User = {
  id: number;
  name: string;
};
type Data = {
  user: User;
  date: Date;
  instance: number;
};

EduardoRFS

# setup dbus
if test -z "$DBUS_SESSION_BUS_ADDRESS"; then
	eval $(dbus-launch --exit-with-session --sh-syntax)
fi
systemctl --user import-environment DISPLAY XAUTHORITY

if command -v dbus-update-activation-environment >/dev/null 2>&1; then
        dbus-update-activation-environment DISPLAY XAUTHORITY
fi

EduardoRFS

%{
open Tree
(*
type expr = Tree.expr =
  | Literal of int
  | Add of (expr * expr)
  | Sub of (expr * expr)
  | Mul of (expr * expr)
  | Div of (expr * expr)
*)

EduardoRFS

[@@@ocaml.warning "-37-32"]

module Name = struct
  type name = string
  type t = name

  module Map = Map.Make (String)
end

module Var : sig

EduardoRFS

Set Universe Polymorphism.

Set Primitive Projections.
Record ssig (A : Type) (P : A -> SProp) : Type := { l : A; r : P l }.

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.

Definition I_Bool (c_b : C_Bool) : SProp :=

EduardoRFS

```rust
// rules
// Those rules are fully church-style
Γ, x : A |- B : Type
---------------------------
Γ |- @self(x : A). B : Type

Γ, x : A |- M : B[x := @fix(x : A). M]  Γ |- A ≂ @self(x : A). B
----------------------------------------------------------------
Γ |- @fix(x : A). M : @self(x : A). B

EduardoRFS

let Closed A = ∀(G : Grade). A [G]
// closed as it is unknown how many copies it will be needed(0..1)
let Bool : Type = ∀(A : Type). Closed A -> Closed A -> Closed A
let true : Closed Bool =
  // safe to ignore y as it is used 0 times
  ΛG. [ΛA. fun x y -> let [y] = y 0 in x]
let false : Closed Bool =
  ΛG. [ΛA. fun x y -> let [y] = x 0 in y]

// same applies to nats but (0..n)

EduardoRFS

data Bool =
  Bool (exists {n : Nat} . exists {m : Nat} .
    (forall {a : Type} . a [n] -> a [m] -> a))

true : Bool
true = 
  let true_ex_m = 
    pack <0, (/\(a : Type) -> \([x] : a [1]) -> \([y] : a [0]) -> x)>
      as exists {m : Nat} .
        (forall {a : Type} . a [1] -> a [m] -> a) in

EduardoRFS

module type T = sig
  module type S
end

module T = struct
  module type S = T
end

module type K_Bool = functor (X : T) (Y : T) -> T

EduardoRFS

// hi
func (wr WorkspaceRepository) CreateWorkspace(workspace *models.Workspace) error {
  result := wr.db.Table("workspaceszz").
				Create(workspace).
				Where("foo").
				Where("foo2");
	return errors.Wrap(
    repository_utils.HandleDatabaseError(result),
		StrWorkspaceRepositoryCreateWorkspaceErr
  )