Skip to content

Instantly share code, notes, and snippets.

View miikka's full-sized avatar

Miikka Koskinen miikka

View GitHub Profile
@miikka
miikka / topology.v
Created January 15, 2016 10:25 — forked from andrejbauer/topology.v
How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.
(* How do to topology in Coq if you are secretly an HOL fan.
We will not use type classes or canonical structures because they
count as "advanced" technology. But we will use notations.
*)
(* We think of subsets as propositional functions.
Thus, if [A] is a type [x : A] and [U] is a subset of [A],
[U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.
from collections import defaultdict, namedtuple
import numpy as np
def visible_cap_central_angle(altitude):
earth_radius = 6371.0
return np.arctan2(np.sqrt(altitude * (altitude + 2 * earth_radius)),
earth_radius)
def hav(x):
return np.sin(x/2)**2