davesnx

module Index = struct
  type t = int * string

  let create i s = (i, s)
  let eq t1 t2 = fst t1 = fst t2
  let enter_level (i, s) = (i + 1, s)
  let pp_index i = Format.sprintf "%s" (snd i)
end

type typ = Tvar | Tpoly | Tfun of typ * typ

davesnx

type _ io =
  | Sync : (unit -> 'a) -> 'a io
  | FlatMap : 'a io * ('a -> 'b io) -> 'b io
  | Async : ((('a -> unit) -> unit) -> unit) -> 'a io
  | All : 'a io list -> 'a list io
  | Sleep : float -> unit io

let flatMap f io = FlatMap (io, f)
let map f io = flatMap (fun a -> Sync (fun () -> f a)) io

EduardoRFS

(*
  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

(*
  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.

BRonen

def tokens:
  split(" ") | map(select(length > 0));

def isnum:
  test("^-?([0-9]+(\\.[0-9]+)?)$");

def evaluate:
  def eval($tokens):
    if ($tokens | length) == 0 then
      error("ending unexpected")

EduardoRFS

(*
  Everything here is really ugly as I didn't clean it,
    some bits come from the Coq-HoTT library.

  The main idea is that given funext and any
    h-set with multiple provably distinct elements.

  Univalence is only used to prove s_true_neq_s_false

  Then by funext you can get the induction principle to contract.

AndrasKovacs

Lightweight region memory management in a two-stage language

• Intro
• Basics
  • Stage inference
• Regions
  • Bit-stealing
  • Using regions
• Eager regions

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

Grubba27

package cripto

import (
	"github.com/ethereum/go-ethereum/accounts"
	"github.com/ethereum/go-ethereum/common/hexutil"
	"github.com/ethereum/go-ethereum/crypto"
)

// from: https://gist.github.com/dcb9/385631846097e1f59e3cba3b1d42f3ed#file-eth_sign_verify-go
func VerifySig(from, sigHex string, msg []byte) bool {

coolaj86

Chat GPT "DAN" (and other "Jailbreaks")

• https://chat.openai.com/
• Is ChatGPT "DAN" Real? Gonna find out [Part 1]
  (https://www.youtube.com/watch?v=-q8woRG9FrI)
• Part 2: I thought ChatGPT DAN was a hoax, but...
  (https://www.youtube.com/watch?v=rHZRrDu3A2U&lc=UgxfrxX8aK7gnCzkend4AaABAg)