pervognsen

This note is in response to this article, particularly the final section on three degrees of freedom:

	http://marc-b-reynolds.github.io/distribution/2017/01/27/UniformRot.html

It notes that "Marsaglia hand-wavingly presented a method for the 4D sphere". I hope to give some insight
into how this method may be obtained and how it relates to some relatively commonplace mathematical ideas.

The unit quaternions may be embedded in C^2 as pairs of complex numbers (z1, z2) satisfying |z1|^2 + |z2|^2 = 1.

If we write z1 and z2 in polar coordinates as z1 = r1 exp(i t1) and z2 = r2 exp(i t2), this is equivalent to

leodemoura

meta def blast : tactic unit := using_smt $ return ()

structure Category :=
  (Obj : Type)
  (Hom : Obj → Obj → Type)

structure Functor (C : Category) (D : Category) :=
  (onObjects   : C^.Obj → D^.Obj)
  (onMorphisms : Π { X Y : C^.Obj },
                C^.Hom X Y → D^.Hom (onObjects X) (onObjects Y))

leodemoura

-- Return the maximum unsigned number of a given width.
def max_unsigned : ℕ → ℕ
| 0 := 0
| (nat.succ x) := 2 * max_unsigned x + 1

open tactic nat

/- Function for convertiong a nat into a Lean expression using nat.zero and nat.succ.
   Remark: the standard library already contains a tactic for converting nat into a binary encoding. -/
meta def nat.to_unary_expr : nat → tactic expr

andrejbauer

(* An initial attempt at universal algebra in Coq.
   Author: Andrej Bauer <Andrej.Bauer@andrej.com>

   If someone knows of a less painful way of doing this, please let me know.

   We would like to define the notion of an algebra with given operations satisfying given
   equations. For example, a group has of three operations (unit, multiplication, inverse)
   and five equations (associativity, unit left, unit right, inverse left, inverse right).
*)

pearcy.py

# -*- coding: utf-8 -*-

import numpy as np
import matplotlib.pyplot as plt
import scipy.integrate as integrate

# Dimension of image in pixels
N = 256
# Number of samples to use for integration
M = 32

samsheffield

// Unity C# Cheat Sheet
// I made these examples for students with prior exerience working with C# and Unity. 
// Too much? Try Unity's very good tutorials to get up to speed: https://unity3d.com/learn/tutorials/topics/scripting

chriseth

This gist shows how formal conditions of Solidity smart contracts can be automatically verified even in the presence of potential re-entrant calls from other contracts.

Solidity already supports formal verification of some contracts that do not make calls to other contracts. This of course excludes any contract that transfers Ether or tokens.

The Solidity contract below models a crude crowdfunding contract that can hold Ether and some person can withdraw Ether according to their shares. It is missing the actual access control, but the point that wants to be made

FreyaHolmer

using UnityEngine;
using System.Linq;

[RequireComponent(typeof(Rigidbody))]
public class RigidbodyMassCalculator : MonoBehaviour {

	public float density = 1f;
	public bool recalculateOnAwake = true;
	
	Rigidbody rb;

wolfiestyle

{-# LANGUAGE BangPatterns #-}

import Control.Applicative
import System.IO
import Data.Maybe
import Data.Complex
import Data.Word
import qualified Data.ByteString as B

data Vec a = Vec { vecx, vecy, vecz :: !a }

leodemoura

open eq

inductive I (F : Type₁ → Prop) : Type₁ :=
mk : I F

axiom InjI : ∀ {x y}, I x = I y → x = y

definition P (x : Type₁) : Prop := ∃ a, I a = x ∧ (a x → false).

definition p := I P