miikka

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

miikka

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