Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/paulch42/lean-spec/llms.txt

Use this file to discover all available pages before exploring further.

LeanSpec.lib.Geo provides the geospatial vocabulary used in the flight-planning specification (FPL) included in the tutorial. It models geographic coordinates and bearings at a level of fidelity sufficient for expressing structural correctness properties — for example, that a route waypoint carries a valid latitude/longitude pair and that a bearing is a value in the correct half-open degree range. The module intentionally avoids computational geometry (great-circle distances, projection, etc.) and imports only LeanSpec.lib.Util for the range-restricted numeric types it needs. All definitions live in the Geo namespace.
The source comment notes that the Longitude type covers the range -180..180 degrees but the original comment in the file reads “-180..100 degrees” — this is a documentation typo in the source; the actual IntMN bounds implement the correct -180..180 range.

​
Unit Conversion

​
degrees2Seconds

Converts a degree value to arc-seconds. This is the foundational conversion used by every constrained coordinate type in the module. 
def degrees2Seconds (deg : Nat) : Nat :=
   deg * 60 * 60
One degree equals 3 600 arc-seconds (60 minutes × 60 seconds per minute). All latitude and longitude values in Geo are stored in arc-seconds to allow integer arithmetic without floating-point imprecision.

​
Coordinate Types

​
Latitude

Geographic latitude expressed in arc-seconds. Valid latitudes span the range −90° to +90° (inclusive on both ends), with positive values representing North and negative values representing South. 
def Latitude := IntMN (-(degrees2Seconds 90)) (degrees2Seconds 90)
deriving DecidableEq
Expanding the bounds: -(degrees2Seconds 90) = -324000 and degrees2Seconds 90 = 324000, so a Latitude value x satisfies -324000 ≤ x < 324000 (the upper bound of IntMN is exclusive, meaning 90° exactly is approached but the type aligns with the half-open convention of IntMN).
IntMN’s upper bound is exclusive. The practical effect is that 90°N (324 000 arc-seconds) is not a member of Latitude. This is a deliberate simplification for the tutorial; a production model would use a closed interval or a separate representation for the poles.
DecidableEq is derived, so latitude values can be compared for equality and used as keys in Map.

​
Longitude

Geographic longitude expressed in arc-seconds. Valid longitudes span the range −180° to +180°, with positive values representing East and negative values representing West. 
def Longitude := IntMN (-(degrees2Seconds 180)) (degrees2Seconds 180)
deriving DecidableEq
Expanding the bounds: -(degrees2Seconds 180) = -648000 and degrees2Seconds 180 = 648000, so a Longitude value x satisfies -648000 ≤ x < 648000. DecidableEq is derived.

​
Composite Types

​
Point

A geographic point on the Earth’s surface, identified by a latitude and a longitude. 
structure Point where
  latitude  : Latitude
  longitude : Longitude
deriving DecidableEq
Both fields carry their range constraints as part of their types, so any Point value is guaranteed to be a valid coordinate pair. DecidableEq is derived, enabling Point values to be compared for equality and used in sets and maps.

​
Direction Types

​
DirectionDatum

The geodetic reference frame (datum) used to express a bearing. Aviation distinguishes between true north (geographic north pole) and magnetic north (the shifting magnetic pole). 
inductive DirectionDatum
  | true
  | magnetic
deriving DecidableEq
ConstructorMeaning
DirectionDatum.trueBearing measured relative to true (geographic) north
DirectionDatum.magneticBearing measured relative to magnetic north
DecidableEq is derived.

​
Direction

A bearing, combining a DirectionDatum with a numeric value in arc-seconds covering the full circle [0°, 360°). 
structure Direction where
  datum : DirectionDatum
  value : NatMN (degrees2Seconds 0) (degrees2Seconds 360)
deriving DecidableEq
The value field is a NatMN with lower bound degrees2Seconds 0 = 0 and upper bound degrees2Seconds 360 = 1296000 (exclusive), so every valid Direction encodes a bearing in [0, 1 296 000) arc-seconds — exactly one full rotation. A value of 0 represents due North; values increase clockwise. DecidableEq is derived, enabling Direction values to be used as keys in Map and as elements of Set.

Build docs developers (and LLMs) love

Get started for freeTalk to us