siraben

{ lib ? (import <nixpkgs> {}).lib }:

with lib;

let
  # Fourth-order Runge-Kutta method
  rk4 = f: x0: y0: z0: h:
    let
      k1_y = z0;
      k1_z = f x0 y0 z0;

siraben

// SPDX-License-Identifier: GPL-3.0

pragma solidity >=0.7.0 <0.9.0;

/**
 * @title Owner
 * @dev Set & change owner
 */
contract Owner {

siraben

((\f. (\x. (f \v. ((x x) v)) \x. (f \v. ((x x) v))) \r. \n. i(n,o,m(n,(r d(n))))) x)

siraben

-- Call-by-value lambda calculus in cool
(*
data Expr = Var Str
          | Abs Str Expr
          | App Expr Expr
          | Sub1 Expr
          | Mul Expr Expr
          | Add Expr Expr
          | Ifz Expr Expr Expr
*)

siraben

siraben

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE TypeOperators #-}

module ExtALaCarte where

siraben

siraben

(* There are no surjections from {1} to {1,2} *)

Definition surjective {A B} (f : A -> B) := forall (b : B), exists (a : A), b = f a.

Definition One := unit.

Definition Two := bool.

Theorem no_surject_one_two : ~ exists (f : One -> Two), surjective f.
Proof.

siraben

(* P is a family of nat-indexed sets of nat such that:
   H: for all n, there is an m such that m ∈ P n
   -----------
   Then we show that there is a choice function f
*)
Theorem countable_choice_wikipedia
  (P : nat -> (nat -> Prop)) (H : forall n, { m | P n m }) : { f | forall n, (exists m, P n m /\ f n = m)}.
Proof.
  set (f := fun (n : nat) => let (m, Hm) := H n in m).
  exists f.

siraben

Require Import ssreflect ssrfun.

Module Futamura.
  (* Program from a -> b written in L *)
  Inductive Program {a b language : Type} :=
  | mkProgram : (a -> b) -> Program.

  Definition runProgram {A B L} (p : @Program A B L) := match p with mkProgram f => f end.
  Notation "[ S | a >> b ]" := (@Program a b S) (at level 2) : type_scope.