Alkanes

Content created by Jonathan Prieto-Cubides, Fredrik Bakke, Egbert Rijke and Amélia Liao.

Created on 2022-07-05.
Last modified on 2024-04-11.

module organic-chemistry.alkanes where
Imports 
open import foundation.universe-levels

open import organic-chemistry.hydrocarbons
open import organic-chemistry.saturated-carbons

Idea

An alkane is a hydrocarbon that only has saturated carbons, i.e., it does not have any double or triple carbon-carbon bonds.

Definition

is-alkane-hydrocarbon : {l1 l2 : Level} → hydrocarbon l1 l2 → UU (l1 ⊔ l2)
is-alkane-hydrocarbon H =
  (c : vertex-hydrocarbon H) → is-saturated-carbon-hydrocarbon H c

Recent changes