...
 
Commits (2)
......@@ -88,7 +88,7 @@ theory ExtendedReals : base:?Logic =
include ?RealArithmetics ❙
// extended_reals : type ❘ # ℝ∞ ❙
// reals_are_extended : ℝ <* ℝ∞ ❙
infty : ℝ ❘ # ∞ prec 1 ❙
infty : ℝ ❘ # ∞ prec 1 ❙
// leq : ℝ∞ ⟶ ℝ∞ ⟶ bool ❘ # 1 ≤ 2 prec 101 ❙
// TODO neginfty : ℝ∞ ❘ = - ∞ ❘ # -∞ ❙