refactor(library/init/algebra): remove order_pair classes
This commit is contained in:
Gabriel Ebner
Leonardo de Moura
parent
4f66673fc2
commit
ce509e621a
16 changed files with 180 additions and 190 deletions
|
|
@ -247,7 +247,7 @@ abs_of_nonneg $ abs_nonneg a
|
|||
lemma le_abs_self (a : α) : a ≤ abs a :=
|
||||
or.elim (le_total 0 a)
|
||||
(assume h : 0 ≤ a,
|
||||
begin rw [abs_of_nonneg h], apply le_refl end)
|
||||
begin rw [abs_of_nonneg h] end)
|
||||
(assume h : a ≤ 0, le_trans h $ abs_nonneg a)
|
||||
|
||||
lemma neg_le_abs_self (a : α) : -a ≤ abs a :=
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.logic
|
||||
import init.logic init.classical
|
||||
/- Make sure instances defined in this file have lower priority than the ones
|
||||
defined for concrete structures -/
|
||||
set_option default_priority 100
|
||||
|
|
@ -14,165 +14,144 @@ set_option old_structure_cmd true
|
|||
universe u
|
||||
variables {α : Type u}
|
||||
|
||||
class weak_order (α : Type u) extends has_le α :=
|
||||
class pre_order (α : Type u) extends has_le α, has_lt α :=
|
||||
(le_refl : ∀ a : α, a ≤ a)
|
||||
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
|
||||
(lt := λ a b, a ≤ b ∧ ¬ b ≤ a)
|
||||
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a))
|
||||
-- TODO(gabriel): default lt_spec to λ a b, iff.refl _
|
||||
|
||||
class partial_order (α : Type u) extends pre_order α :=
|
||||
(le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)
|
||||
|
||||
class linear_weak_order (α : Type u) extends weak_order α :=
|
||||
class linear_order (α : Type u) extends partial_order α :=
|
||||
(le_total : ∀ a b : α, a ≤ b ∨ b ≤ a)
|
||||
|
||||
class strict_order (α : Type u) extends has_lt α :=
|
||||
(lt_irrefl : ∀ a : α, ¬ a < a)
|
||||
(lt_trans : ∀ a b c : α, a < b → b < c → a < c)
|
||||
@[refl] lemma le_refl [pre_order α] : ∀ a : α, a ≤ a :=
|
||||
pre_order.le_refl
|
||||
|
||||
/- structures with a weak and a strict order -/
|
||||
class order_pair (α : Type u) extends weak_order α, has_lt α :=
|
||||
(le_of_lt : ∀ a b : α, a < b → a ≤ b)
|
||||
(lt_of_lt_of_le : ∀ a b c : α, a < b → b ≤ c → a < c)
|
||||
(lt_of_le_of_lt : ∀ a b c : α, a ≤ b → b < c → a < c)
|
||||
(lt_irrefl : ∀ a : α, ¬ a < a)
|
||||
@[trans] lemma le_trans [pre_order α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
|
||||
pre_order.le_trans
|
||||
|
||||
class strong_order_pair (α : Type u) extends weak_order α, has_lt α :=
|
||||
(le_iff_lt_or_eq : ∀ a b : α, a ≤ b ↔ a < b ∨ a = b)
|
||||
(lt_irrefl : ∀ a : α, ¬ a < a)
|
||||
lemma lt_of_le_not_le [pre_order α] : ∀ {a b : α}, a ≤ b → ¬ b ≤ a → a < b
|
||||
| a b hab hba := (pre_order.lt_iff_le_not_le _ _).mpr ⟨hab, hba⟩
|
||||
|
||||
class linear_order_pair (α : Type u) extends order_pair α, linear_weak_order α
|
||||
lemma le_not_le_of_lt [pre_order α] : ∀ {a b : α}, a < b → a ≤ b ∧ ¬ b ≤ a
|
||||
| a b hab := (pre_order.lt_iff_le_not_le _ _).mp hab
|
||||
|
||||
class linear_strong_order_pair (α : Type u) extends strong_order_pair α, linear_weak_order α
|
||||
lemma le_antisymm [partial_order α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
|
||||
partial_order.le_antisymm
|
||||
|
||||
@[refl] lemma le_refl [weak_order α] : ∀ a : α, a ≤ a :=
|
||||
weak_order.le_refl
|
||||
|
||||
@[trans] lemma le_trans [weak_order α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=
|
||||
weak_order.le_trans
|
||||
|
||||
lemma le_antisymm [weak_order α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
|
||||
weak_order.le_antisymm
|
||||
|
||||
lemma le_of_eq [weak_order α] {a b : α} : a = b → a ≤ b :=
|
||||
lemma le_of_eq [partial_order α] {a b : α} : a = b → a ≤ b :=
|
||||
λ h, h ▸ le_refl a
|
||||
|
||||
lemma le_antisymm_iff [weak_order α] {a b : α} : a = b ↔ a ≤ b ∧ b ≤ a :=
|
||||
lemma le_antisymm_iff [partial_order α] {a b : α} : a = b ↔ a ≤ b ∧ b ≤ a :=
|
||||
⟨λe, ⟨le_of_eq e, le_of_eq e.symm⟩, λ⟨h1, h2⟩, le_antisymm h1 h2⟩
|
||||
|
||||
@[trans] lemma ge_trans [weak_order α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c :=
|
||||
@[trans] lemma ge_trans [pre_order α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c :=
|
||||
λ a b c h₁ h₂, le_trans h₂ h₁
|
||||
|
||||
lemma le_total [linear_weak_order α] : ∀ a b : α, a ≤ b ∨ b ≤ a :=
|
||||
linear_weak_order.le_total
|
||||
lemma le_total [linear_order α] : ∀ a b : α, a ≤ b ∨ b ≤ a :=
|
||||
linear_order.le_total
|
||||
|
||||
lemma le_of_not_ge [linear_weak_order α] {a b : α} : ¬ a ≥ b → a ≤ b :=
|
||||
lemma le_of_not_ge [linear_order α] {a b : α} : ¬ a ≥ b → a ≤ b :=
|
||||
or.resolve_left (le_total b a)
|
||||
|
||||
lemma le_of_not_le [linear_weak_order α] {a b : α} : ¬ a ≤ b → b ≤ a :=
|
||||
lemma le_of_not_le [linear_order α] {a b : α} : ¬ a ≤ b → b ≤ a :=
|
||||
or.resolve_left (le_total a b)
|
||||
|
||||
lemma lt_irrefl [strict_order α] : ∀ a : α, ¬ a < a :=
|
||||
strict_order.lt_irrefl
|
||||
lemma lt_irrefl [pre_order α] : ∀ a : α, ¬ a < a
|
||||
| a haa := match le_not_le_of_lt haa with
|
||||
| ⟨h1, h2⟩ := false.rec _ (h2 h1)
|
||||
end
|
||||
|
||||
lemma gt_irrefl [strict_order α] : ∀ a : α, ¬ a > a :=
|
||||
lemma gt_irrefl [pre_order α] : ∀ a : α, ¬ a > a :=
|
||||
lt_irrefl
|
||||
|
||||
@[trans] lemma lt_trans [strict_order α] : ∀ {a b c : α}, a < b → b < c → a < c :=
|
||||
strict_order.lt_trans
|
||||
@[trans] lemma lt_trans [pre_order α] : ∀ {a b c : α}, a < b → b < c → a < c
|
||||
| a b c hab hbc :=
|
||||
match le_not_le_of_lt hab, le_not_le_of_lt hbc with
|
||||
| ⟨hab, hba⟩, ⟨hbc, hcb⟩ := lt_of_le_not_le (le_trans hab hbc) (λ hca, hcb (le_trans hca hab))
|
||||
end
|
||||
|
||||
def lt.trans := @lt_trans
|
||||
|
||||
@[trans] lemma gt_trans [strict_order α] : ∀ {a b c : α}, a > b → b > c → a > c :=
|
||||
@[trans] lemma gt_trans [pre_order α] : ∀ {a b c : α}, a > b → b > c → a > c :=
|
||||
λ a b c h₁ h₂, lt_trans h₂ h₁
|
||||
|
||||
def gt.trans := @gt_trans
|
||||
|
||||
lemma ne_of_lt [strict_order α] {a b : α} (h : a < b) : a ≠ b :=
|
||||
lemma ne_of_lt [pre_order α] {a b : α} (h : a < b) : a ≠ b :=
|
||||
λ he, absurd h (he ▸ lt_irrefl a)
|
||||
|
||||
lemma ne_of_gt [strict_order α] {a b : α} (h : a > b) : a ≠ b :=
|
||||
lemma ne_of_gt [pre_order α] {a b : α} (h : a > b) : a ≠ b :=
|
||||
λ he, absurd h (he ▸ lt_irrefl a)
|
||||
|
||||
lemma lt_asymm [strict_order α] {a b : α} (h : a < b) : ¬ b < a :=
|
||||
lemma lt_asymm [pre_order α] {a b : α} (h : a < b) : ¬ b < a :=
|
||||
λ h1 : b < a, lt_irrefl a (lt_trans h h1)
|
||||
|
||||
lemma not_lt_of_gt [strict_order α] {a b : α} (h : a > b) : ¬ a < b :=
|
||||
lemma not_lt_of_gt [linear_order α] {a b : α} (h : a > b) : ¬ a < b :=
|
||||
lt_asymm h
|
||||
|
||||
lemma le_of_lt [order_pair α] : ∀ {a b : α}, a < b → a ≤ b :=
|
||||
order_pair.le_of_lt
|
||||
lemma le_of_lt [pre_order α] : ∀ {a b : α}, a < b → a ≤ b
|
||||
| a b hab := (le_not_le_of_lt hab).left
|
||||
|
||||
@[trans] lemma lt_of_lt_of_le [order_pair α] : ∀ {a b c : α}, a < b → b ≤ c → a < c :=
|
||||
order_pair.lt_of_lt_of_le
|
||||
@[trans] lemma lt_of_lt_of_le [pre_order α] : ∀ {a b c : α}, a < b → b ≤ c → a < c
|
||||
| a b c hab hbc :=
|
||||
let ⟨hab, hba⟩ := le_not_le_of_lt hab in
|
||||
lt_of_le_not_le (le_trans hab hbc) $ λ hca, hba (le_trans hbc hca)
|
||||
|
||||
@[trans] lemma lt_of_le_of_lt [order_pair α] : ∀ {a b c : α}, a ≤ b → b < c → a < c :=
|
||||
order_pair.lt_of_le_of_lt
|
||||
@[trans] lemma lt_of_le_of_lt [pre_order α] : ∀ {a b c : α}, a ≤ b → b < c → a < c
|
||||
| a b c hab hbc :=
|
||||
let ⟨hbc, hcb⟩ := le_not_le_of_lt hbc in
|
||||
lt_of_le_not_le (le_trans hab hbc) $ λ hca, hcb (le_trans hca hab)
|
||||
|
||||
@[trans] lemma gt_of_gt_of_ge [order_pair α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c :=
|
||||
@[trans] lemma gt_of_gt_of_ge [pre_order α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c :=
|
||||
lt_of_le_of_lt h₂ h₁
|
||||
|
||||
@[trans] lemma gt_of_ge_of_gt [order_pair α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c :=
|
||||
@[trans] lemma gt_of_ge_of_gt [pre_order α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c :=
|
||||
lt_of_lt_of_le h₂ h₁
|
||||
|
||||
instance order_pair.to_strict_order [s : order_pair α] : strict_order α :=
|
||||
{ s with
|
||||
lt_irrefl := order_pair.lt_irrefl,
|
||||
lt_trans := λ a b c h₁ h₂, lt_of_lt_of_le h₁ (le_of_lt h₂) }
|
||||
lemma not_le_of_gt [pre_order α] {a b : α} (h : a > b) : ¬ a ≤ b :=
|
||||
(le_not_le_of_lt h).right
|
||||
|
||||
lemma not_le_of_gt [order_pair α] {a b : α} (h : a > b) : ¬ a ≤ b :=
|
||||
λ h₁, lt_irrefl b (lt_of_lt_of_le h h₁)
|
||||
lemma not_lt_of_ge [pre_order α] {a b : α} (h : a ≥ b) : ¬ a < b :=
|
||||
λ hab, not_le_of_gt hab h
|
||||
|
||||
lemma not_lt_of_ge [order_pair α] {a b : α} (h : a ≥ b) : ¬ a < b :=
|
||||
λ h₁, lt_irrefl b (lt_of_le_of_lt h h₁)
|
||||
lemma lt_or_eq_of_le [partial_order α] : ∀ {a b : α}, a ≤ b → a < b ∨ a = b
|
||||
| a b hab := classical.by_cases
|
||||
(λ hba : b ≤ a, or.inr (le_antisymm hab hba))
|
||||
(λ hba, or.inl (lt_of_le_not_le hab hba))
|
||||
|
||||
lemma le_iff_lt_or_eq [strong_order_pair α] : ∀ {a b : α}, a ≤ b ↔ a < b ∨ a = b :=
|
||||
strong_order_pair.le_iff_lt_or_eq
|
||||
lemma le_of_lt_or_eq [partial_order α] : ∀ {a b : α}, (a < b ∨ a = b) → a ≤ b
|
||||
| a b (or.inl hab) := le_of_lt hab
|
||||
| a b (or.inr hab) := hab ▸ le_refl _
|
||||
|
||||
lemma lt_or_eq_of_le [strong_order_pair α] : ∀ {a b : α}, a ≤ b → a < b ∨ a = b :=
|
||||
λ a b h, iff.mp le_iff_lt_or_eq h
|
||||
lemma le_iff_lt_or_eq [partial_order α] : ∀ {a b : α}, a ≤ b ↔ a < b ∨ a = b
|
||||
| a b := ⟨lt_or_eq_of_le, le_of_lt_or_eq⟩
|
||||
|
||||
lemma le_of_lt_or_eq [strong_order_pair α] : ∀ {a b : α}, (a < b ∨ a = b) → a ≤ b :=
|
||||
λ a b h, iff.mpr le_iff_lt_or_eq h
|
||||
|
||||
lemma lt_of_le_of_ne [strong_order_pair α] {a b : α} : a ≤ b → a ≠ b → a < b :=
|
||||
lemma lt_of_le_of_ne [partial_order α] {a b : α} : a ≤ b → a ≠ b → a < b :=
|
||||
λ h₁ h₂, or.resolve_right (lt_or_eq_of_le h₁) h₂
|
||||
|
||||
private lemma lt_irrefl' [strong_order_pair α] : ∀ a : α, ¬ a < a :=
|
||||
strong_order_pair.lt_irrefl
|
||||
-- private lemma lt_of_lt_of_le' [strong_order_pair α] (a b c : α) (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
|
||||
-- have a ≤ c, from le_trans (le_of_lt' h₁) h₂,
|
||||
-- or.elim (lt_or_eq_of_le this)
|
||||
-- (λ h : a < c, h)
|
||||
-- (λ h : a = c,
|
||||
-- have b ≤ a, from h.symm ▸ h₂,
|
||||
-- have a = b, from le_antisymm (le_of_lt' h₁) this,
|
||||
-- absurd h₁ (this ▸ lt_irrefl' a))
|
||||
|
||||
private lemma le_of_lt' [strong_order_pair α] ⦃a b : α⦄ (h : a < b) : a ≤ b :=
|
||||
le_of_lt_or_eq (or.inl h)
|
||||
-- private lemma lt_of_le_of_lt' [strong_order_pair α] (a b c : α) (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
|
||||
-- have a ≤ c, from le_trans h₁ (le_of_lt' h₂),
|
||||
-- or.elim (lt_or_eq_of_le this)
|
||||
-- (λ h : a < c, h)
|
||||
-- (λ h : a = c,
|
||||
-- have c ≤ b, from h ▸ h₁,
|
||||
-- have c = b, from le_antisymm this (le_of_lt' h₂),
|
||||
-- absurd h₂ (this ▸ lt_irrefl' c))
|
||||
|
||||
private lemma lt_of_lt_of_le' [strong_order_pair α] (a b c : α) (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
|
||||
have a ≤ c, from le_trans (le_of_lt' h₁) h₂,
|
||||
or.elim (lt_or_eq_of_le this)
|
||||
(λ h : a < c, h)
|
||||
(λ h : a = c,
|
||||
have b ≤ a, from h.symm ▸ h₂,
|
||||
have a = b, from le_antisymm (le_of_lt' h₁) this,
|
||||
absurd h₁ (this ▸ lt_irrefl' a))
|
||||
|
||||
private lemma lt_of_le_of_lt' [strong_order_pair α] (a b c : α) (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
|
||||
have a ≤ c, from le_trans h₁ (le_of_lt' h₂),
|
||||
or.elim (lt_or_eq_of_le this)
|
||||
(λ h : a < c, h)
|
||||
(λ h : a = c,
|
||||
have c ≤ b, from h ▸ h₁,
|
||||
have c = b, from le_antisymm this (le_of_lt' h₂),
|
||||
absurd h₂ (this ▸ lt_irrefl' c))
|
||||
|
||||
instance strong_order_pair.to_order_pair [s : strong_order_pair α] : order_pair α :=
|
||||
{ s with
|
||||
lt_irrefl := lt_irrefl',
|
||||
le_of_lt := le_of_lt',
|
||||
lt_of_le_of_lt := lt_of_le_of_lt',
|
||||
lt_of_lt_of_le := lt_of_lt_of_le'}
|
||||
|
||||
instance linear_strong_order_pair.to_linear_order_pair [s : linear_strong_order_pair α] : linear_order_pair α :=
|
||||
{ s with
|
||||
lt_irrefl := lt_irrefl',
|
||||
le_of_lt := le_of_lt',
|
||||
lt_of_le_of_lt := lt_of_le_of_lt',
|
||||
lt_of_lt_of_le := lt_of_lt_of_le'}
|
||||
|
||||
lemma lt_trichotomy [linear_strong_order_pair α] (a b : α) : a < b ∨ a = b ∨ b < a :=
|
||||
lemma lt_trichotomy [linear_order α] (a b : α) : a < b ∨ a = b ∨ b < a :=
|
||||
or.elim (le_total a b)
|
||||
(λ h : a ≤ b, or.elim (lt_or_eq_of_le h)
|
||||
(λ h : a < b, or.inl h)
|
||||
|
|
@ -181,67 +160,72 @@ or.elim (le_total a b)
|
|||
(λ h : b < a, or.inr (or.inr h))
|
||||
(λ h : b = a, or.inr (or.inl h.symm)))
|
||||
|
||||
|
||||
lemma le_of_not_gt [linear_strong_order_pair α] {a b : α} (h : ¬ a > b) : a ≤ b :=
|
||||
lemma le_of_not_gt [linear_order α] {a b : α} (h : ¬ a > b) : a ≤ b :=
|
||||
match lt_trichotomy a b with
|
||||
| or.inl hlt := le_of_lt hlt
|
||||
| or.inr (or.inl heq) := heq ▸ le_refl a
|
||||
| or.inr (or.inr hgt) := absurd hgt h
|
||||
end
|
||||
|
||||
lemma lt_of_not_ge [linear_strong_order_pair α] {a b : α} (h : ¬ a ≥ b) : a < b :=
|
||||
lemma lt_of_not_ge [linear_order α] {a b : α} (h : ¬ a ≥ b) : a < b :=
|
||||
match lt_trichotomy a b with
|
||||
| or.inl hlt := hlt
|
||||
| or.inr (or.inl heq) := absurd (heq ▸ le_refl a : a ≥ b) h
|
||||
| or.inr (or.inr hgt) := absurd (le_of_lt hgt) h
|
||||
end
|
||||
|
||||
lemma lt_or_ge [linear_strong_order_pair α] (a b : α) : a < b ∨ a ≥ b :=
|
||||
lemma lt_or_ge [linear_order α] (a b : α) : a < b ∨ a ≥ b :=
|
||||
match lt_trichotomy a b with
|
||||
| or.inl hlt := or.inl hlt
|
||||
| or.inr (or.inl heq) := or.inr (heq ▸ le_refl a)
|
||||
| or.inr (or.inr hgt) := or.inr (le_of_lt hgt)
|
||||
end
|
||||
|
||||
lemma le_or_gt [linear_strong_order_pair α] (a b : α) : a ≤ b ∨ a > b :=
|
||||
lemma le_or_gt [linear_order α] (a b : α) : a ≤ b ∨ a > b :=
|
||||
or.swap (lt_or_ge b a)
|
||||
|
||||
lemma lt_or_gt_of_ne [linear_strong_order_pair α] {a b : α} (h : a ≠ b) : a < b ∨ a > b :=
|
||||
lemma lt_or_gt_of_ne [linear_order α] {a b : α} (h : a ≠ b) : a < b ∨ a > b :=
|
||||
match lt_trichotomy a b with
|
||||
| or.inl hlt := or.inl hlt
|
||||
| or.inr (or.inl heq) := absurd heq h
|
||||
| or.inr (or.inr hgt) := or.inr hgt
|
||||
end
|
||||
|
||||
lemma ne_iff_lt_or_gt [linear_strong_order_pair α] {a b : α} : a ≠ b ↔ a < b ∨ a > b :=
|
||||
lemma ne_iff_lt_or_gt [linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ a > b :=
|
||||
⟨lt_or_gt_of_ne, λo, or.elim o ne_of_lt ne_of_gt⟩
|
||||
|
||||
lemma lt_iff_not_ge [linear_strong_order_pair α] (x y : α) : x < y ↔ ¬ x ≥ y :=
|
||||
lemma lt_iff_not_ge [linear_order α] (x y : α) : x < y ↔ ¬ x ≥ y :=
|
||||
⟨not_le_of_gt, lt_of_not_ge⟩
|
||||
|
||||
/- The following lemma can be used when defining a decidable_linear_order instance, and the concrete structure
|
||||
does not have its own definition for decidable le -/
|
||||
def decidable_le_of_decidable_lt [linear_strong_order_pair α] [∀ a b : α, decidable (a < b)] (a b : α) : decidable (a ≤ b) :=
|
||||
if h₁ : a < b then is_true (le_of_lt h₁)
|
||||
else if h₂ : b < a then is_false (not_le_of_gt h₂)
|
||||
else is_true (le_of_not_gt h₂)
|
||||
instance decidable_lt_of_decidable_le [pre_order α]
|
||||
[decidable_rel ((≤) : α → α → Prop)] :
|
||||
decidable_rel ((<) : α → α → Prop)
|
||||
| a b :=
|
||||
if hab : a ≤ b then
|
||||
if hba : b ≤ a then
|
||||
is_false $ λ hab', not_le_of_gt hab' hba
|
||||
else
|
||||
is_true $ lt_of_le_not_le hab hba
|
||||
else
|
||||
is_false $ λ hab', hab (le_of_lt hab')
|
||||
|
||||
/- The following lemma can be used when defining a decidable_linear_order instance, and the concrete structure
|
||||
does not have its own definition for decidable le -/
|
||||
def decidable_eq_of_decidable_lt [linear_strong_order_pair α] [∀ a b : α, decidable (a < b)] (a b : α) : decidable (a = b) :=
|
||||
match decidable_le_of_decidable_lt a b with
|
||||
| is_true h₁ :=
|
||||
match decidable_le_of_decidable_lt b a with
|
||||
| is_true h₂ := is_true (le_antisymm h₁ h₂)
|
||||
| is_false h₂ := is_false (λ he : a = b, h₂ (he ▸ le_refl a))
|
||||
end
|
||||
| is_false h₁ := is_false (λ he : a = b, h₁ (he ▸ le_refl a))
|
||||
end
|
||||
instance decidable_eq_of_decidable_le [partial_order α]
|
||||
[decidable_rel ((≤) : α → α → Prop)] :
|
||||
decidable_eq α
|
||||
| a b :=
|
||||
if hab : a ≤ b then
|
||||
if hba : b ≤ a then
|
||||
is_true (le_antisymm hab hba)
|
||||
else
|
||||
is_false (λ heq, hba (heq ▸ le_refl _))
|
||||
else
|
||||
is_false (λ heq, hab (heq ▸ le_refl _))
|
||||
|
||||
class decidable_linear_order (α : Type u) extends linear_strong_order_pair α :=
|
||||
(decidable_lt : decidable_rel lt)
|
||||
(decidable_le : decidable_rel le) -- TODO(Leo): add default value using decidable_le_of_decidable_lt
|
||||
(decidable_eq : decidable_eq α) -- TODO(Leo): add default value using decidable_eq_of_decidable_lt
|
||||
-- TODO(leo,gabriel): add default values
|
||||
class decidable_linear_order (α : Type u) extends linear_order α :=
|
||||
(decidable_le : decidable_rel le)
|
||||
(decidable_eq : decidable_eq α)
|
||||
(decidable_lt : decidable_rel ((<) : α → α → Prop))
|
||||
|
||||
instance [decidable_linear_order α] (a b : α) : decidable (a < b) :=
|
||||
decidable_linear_order.decidable_lt α a b
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ universe u
|
|||
|
||||
class ordered_cancel_comm_monoid (α : Type u)
|
||||
extends add_comm_monoid α, add_left_cancel_semigroup α,
|
||||
add_right_cancel_semigroup α, order_pair α :=
|
||||
add_right_cancel_semigroup α, partial_order α :=
|
||||
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
|
||||
(le_of_add_le_add_left : ∀ a b c : α, a + b ≤ a + c → b ≤ c)
|
||||
(add_lt_add_left : ∀ a b : α, a < b → ∀ c : α, c + a < c + b)
|
||||
|
|
@ -183,7 +183,7 @@ add_zero c ▸ add_lt_add hbc ha
|
|||
|
||||
end ordered_cancel_comm_monoid
|
||||
|
||||
class ordered_comm_group (α : Type u) extends add_comm_group α, order_pair α :=
|
||||
class ordered_comm_group (α : Type u) extends add_comm_group α, partial_order α :=
|
||||
(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
|
||||
(add_lt_add_left : ∀ a b : α, a < b → ∀ c : α, c + a < c + b)
|
||||
|
||||
|
|
@ -615,10 +615,7 @@ class decidable_linear_ordered_comm_group (α : Type u)
|
|||
|
||||
instance decidable_linear_ordered_comm_group.to_ordered_comm_group (α : Type u)
|
||||
[s : decidable_linear_ordered_comm_group α] : ordered_comm_group α :=
|
||||
{s with
|
||||
le_of_lt := @le_of_lt α _,
|
||||
lt_of_le_of_lt := @lt_of_le_of_lt α _,
|
||||
lt_of_lt_of_le := @lt_of_lt_of_le α _ }
|
||||
{ s with add := s.add }
|
||||
|
||||
class decidable_linear_ordered_cancel_comm_monoid (α : Type u)
|
||||
extends ordered_cancel_comm_monoid α, decidable_linear_order α
|
||||
|
|
|
|||
|
|
@ -86,7 +86,7 @@ lemma mul_self_lt_mul_self {a b : α} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b *
|
|||
mul_lt_mul' (le_of_lt h2) h2 h1 (lt_of_le_of_lt h1 h2)
|
||||
end ordered_semiring
|
||||
|
||||
class linear_ordered_semiring (α : Type u) extends ordered_semiring α, linear_strong_order_pair α :=
|
||||
class linear_ordered_semiring (α : Type u) extends ordered_semiring α, linear_order α :=
|
||||
(zero_lt_one : zero < one)
|
||||
|
||||
section linear_ordered_semiring
|
||||
|
|
@ -258,8 +258,8 @@ by rwa zero_mul at this
|
|||
|
||||
end ordered_ring
|
||||
|
||||
class linear_ordered_ring (α : Type u) extends ordered_ring α, linear_strong_order_pair α :=
|
||||
(zero_lt_one : lt zero one)
|
||||
class linear_ordered_ring (α : Type u) extends ordered_ring α, linear_order α :=
|
||||
(zero_lt_one : zero < one)
|
||||
|
||||
instance linear_ordered_ring.to_linear_ordered_semiring [s : linear_ordered_ring α] : linear_ordered_semiring α :=
|
||||
{ s with
|
||||
|
|
|
|||
|
|
@ -207,6 +207,13 @@ iff.mpr
|
|||
(int.lt_iff_le_and_ne _ _)
|
||||
(and.intro hac (assume heq, int.not_le_of_gt begin rw heq, exact hbc end hab))
|
||||
|
||||
protected lemma lt_iff_le_not_le {a b : ℤ} : a < b ↔ (a ≤ b ∧ ¬ b ≤ a) :=
|
||||
begin
|
||||
simp [int.lt_iff_le_and_ne], split; intro h; cases h with hneq hab; split,
|
||||
{assumption}, {intro hba, apply hneq, apply int.le_antisymm; assumption},
|
||||
{intro heq, apply hab, subst heq, apply int.le_refl}, {assumption}
|
||||
end
|
||||
|
||||
instance : decidable_linear_ordered_comm_ring int :=
|
||||
{ int.comm_ring with
|
||||
le := int.le,
|
||||
|
|
@ -214,16 +221,12 @@ instance : decidable_linear_ordered_comm_ring int :=
|
|||
le_trans := @int.le_trans,
|
||||
le_antisymm := @int.le_antisymm,
|
||||
lt := int.lt,
|
||||
le_of_lt := @int.le_of_lt,
|
||||
lt_of_lt_of_le := @int.lt_of_lt_of_le,
|
||||
lt_of_le_of_lt := @int.lt_of_le_of_lt,
|
||||
lt_irrefl := int.lt_irrefl,
|
||||
lt_iff_le_not_le := @int.lt_iff_le_not_le,
|
||||
add_le_add_left := @int.add_le_add_left,
|
||||
add_lt_add_left := @int.add_lt_add_left,
|
||||
zero_ne_one := zero_ne_one,
|
||||
mul_nonneg := @int.mul_nonneg,
|
||||
mul_pos := @int.mul_pos,
|
||||
le_iff_lt_or_eq := int.le_iff_lt_or_eq,
|
||||
le_total := int.le_total,
|
||||
zero_lt_one := int.zero_lt_one,
|
||||
decidable_eq := int.decidable_eq,
|
||||
|
|
|
|||
|
|
@ -187,8 +187,36 @@ lemma lt_succ_self (n : ℕ) : n < succ n := lt.base n
|
|||
protected lemma le_antisymm {n m : ℕ} (h₁ : n ≤ m) : m ≤ n → n = m :=
|
||||
less_than_or_equal.cases_on h₁ (λ a, rfl) (λ a b c, absurd (nat.lt_of_le_of_lt b c) (nat.lt_irrefl n))
|
||||
|
||||
instance : weak_order ℕ :=
|
||||
⟨@nat.less_than_or_equal, @nat.le_refl, @nat.le_trans, @nat.le_antisymm⟩
|
||||
protected lemma lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b
|
||||
| a 0 := or.inr (zero_le a)
|
||||
| a (b+1) :=
|
||||
match lt_or_ge a b with
|
||||
| or.inl h := or.inl (le_succ_of_le h)
|
||||
| or.inr h :=
|
||||
match nat.eq_or_lt_of_le h with
|
||||
| or.inl h1 := or.inl (h1 ▸ lt_succ_self b)
|
||||
| or.inr h1 := or.inr h1
|
||||
end
|
||||
end
|
||||
|
||||
protected lemma le_total {m n : ℕ} : m ≤ n ∨ n ≤ m :=
|
||||
or.imp_left nat.le_of_lt (nat.lt_or_ge m n)
|
||||
|
||||
protected lemma lt_of_le_and_ne {m n : ℕ} (h1 : m ≤ n) : m ≠ n → m < n :=
|
||||
or.resolve_right (or.swap (nat.eq_or_lt_of_le h1))
|
||||
|
||||
protected lemma lt_iff_le_not_le {m n : ℕ} : m < n ↔ (m ≤ n ∧ ¬ n ≤ m) :=
|
||||
⟨λ hmn, ⟨nat.le_of_lt hmn, λ hnm, nat.lt_irrefl _ (nat.lt_of_le_of_lt hnm hmn)⟩,
|
||||
λ ⟨hmn, hnm⟩, nat.lt_of_le_and_ne hmn (λ heq, hnm (heq ▸ nat.le_refl _))⟩
|
||||
|
||||
instance : linear_order ℕ :=
|
||||
{ le := nat.less_than_or_equal,
|
||||
le_refl := @nat.le_refl,
|
||||
le_trans := @nat.le_trans,
|
||||
le_antisymm := @nat.le_antisymm,
|
||||
le_total := @nat.le_total,
|
||||
lt := nat.lt,
|
||||
lt_iff_le_not_le := @nat.lt_iff_le_not_le }
|
||||
|
||||
lemma eq_zero_of_le_zero {n : nat} (h : n ≤ 0) : n = 0 :=
|
||||
le_antisymm h (zero_le _)
|
||||
|
|
@ -210,18 +238,6 @@ lemma pred_lt_pred : ∀ {n m : ℕ}, n ≠ 0 → m ≠ 0 → n < m → pred n <
|
|||
| _ 0 h₁ h₂ h := absurd rfl h₂
|
||||
| (succ n) (succ m) _ _ h := lt_of_succ_lt_succ h
|
||||
|
||||
protected lemma lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b
|
||||
| a 0 := or.inr (zero_le a)
|
||||
| a (b+1) :=
|
||||
match lt_or_ge a b with
|
||||
| or.inl h := or.inl (le_succ_of_le h)
|
||||
| or.inr h :=
|
||||
match nat.eq_or_lt_of_le h with
|
||||
| or.inl h1 := or.inl (h1 ▸ lt_succ_self b)
|
||||
| or.inr h1 := or.inr h1
|
||||
end
|
||||
end
|
||||
|
||||
lemma lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h
|
||||
|
||||
lemma succ_le_of_lt {a b : ℕ} (h : a < b) : succ a ≤ b := h
|
||||
|
|
@ -270,9 +286,6 @@ end
|
|||
protected lemma add_le_add_iff_le_right (k n m : ℕ) : n + k ≤ m + k ↔ n ≤ m :=
|
||||
⟨ nat.le_of_add_le_add_right , assume h, nat.add_le_add_right h _ ⟩
|
||||
|
||||
protected lemma lt_of_le_and_ne {m n : ℕ} (h1 : m ≤ n) : m ≠ n → m < n :=
|
||||
or.resolve_right (or.swap (nat.eq_or_lt_of_le h1))
|
||||
|
||||
protected theorem lt_of_add_lt_add_left {k n m : ℕ} (h : k + n < k + m) : n < m :=
|
||||
let h' := nat.le_of_lt h in
|
||||
nat.lt_of_le_and_ne
|
||||
|
|
@ -294,9 +307,6 @@ by rw add_comm; exact nat.lt_add_of_pos_right h
|
|||
protected lemma zero_lt_one : 0 < (1:nat) :=
|
||||
zero_lt_succ 0
|
||||
|
||||
protected lemma le_total {m n : ℕ} : m ≤ n ∨ n ≤ m :=
|
||||
or.imp_left nat.le_of_lt (nat.lt_or_ge m n)
|
||||
|
||||
protected lemma le_of_lt_or_eq {m n : ℕ} (h : m < n ∨ m = n) : m ≤ n :=
|
||||
nat.le_of_eq_or_lt (or.swap h)
|
||||
|
||||
|
|
@ -332,12 +342,8 @@ instance : decidable_linear_ordered_semiring nat :=
|
|||
le_trans := @nat.le_trans,
|
||||
le_antisymm := @nat.le_antisymm,
|
||||
le_total := @nat.le_total,
|
||||
le_iff_lt_or_eq := @nat.le_iff_lt_or_eq,
|
||||
le_of_lt := @nat.le_of_lt,
|
||||
lt_irrefl := @nat.lt_irrefl,
|
||||
lt_of_lt_of_le := @nat.lt_of_lt_of_le,
|
||||
lt_of_le_of_lt := @nat.lt_of_le_of_lt,
|
||||
lt_of_add_lt_add_left := @nat.lt_of_add_lt_add_left,
|
||||
lt_iff_le_not_le := pre_order.lt_iff_le_not_le,
|
||||
add_lt_add_left := @nat.add_lt_add_left,
|
||||
add_le_add_left := @nat.add_le_add_left,
|
||||
le_of_add_le_add_left := @nat.le_of_add_le_add_left,
|
||||
|
|
|
|||
|
|
@ -75,7 +75,7 @@ expr arith_instance::mk_le() { return mk_op(get_has_le_le_name(), get_has_le_nam
|
|||
|
||||
expr arith_instance::mk_bit0() { return mk_op(get_bit0_name(), get_has_add_name(), m_info->m_bit0); }
|
||||
|
||||
expr arith_instance::mk_weark_order() { return mk_structure(get_weak_order_name(), m_info->m_weak_order); }
|
||||
expr arith_instance::mk_partial_order() { return mk_structure(get_partial_order_name(), m_info->m_partial_order); }
|
||||
expr arith_instance::mk_add_comm_semigroup() { return mk_structure(get_add_comm_semigroup_name(), m_info->m_add_comm_semigroup); }
|
||||
expr arith_instance::mk_monoid() { return mk_structure(get_monoid_name(), m_info->m_monoid); }
|
||||
expr arith_instance::mk_add_monoid() { return mk_structure(get_add_monoid_name(), m_info->m_add_monoid); }
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ class arith_instance_info {
|
|||
optional<expr> m_bit0, m_bit1;
|
||||
|
||||
/* Structures */
|
||||
optional<expr> m_weak_order;
|
||||
optional<expr> m_partial_order;
|
||||
optional<expr> m_add_comm_semigroup;
|
||||
optional<expr> m_monoid, m_add_monoid;
|
||||
optional<expr> m_add_group, m_add_comm_group;
|
||||
|
|
@ -86,7 +86,7 @@ public:
|
|||
expr mk_has_lt() { return app_arg(mk_lt()); }
|
||||
expr mk_has_le() { return app_arg(mk_le()); }
|
||||
|
||||
expr mk_weark_order();
|
||||
expr mk_partial_order();
|
||||
expr mk_add_comm_semigroup();
|
||||
expr mk_monoid();
|
||||
expr mk_add_monoid();
|
||||
|
|
|
|||
|
|
@ -368,7 +368,7 @@ name const * g_unit_star = nullptr;
|
|||
name const * g_unsafe_monad_from_pure_bind = nullptr;
|
||||
name const * g_user_attribute = nullptr;
|
||||
name const * g_vm_monitor = nullptr;
|
||||
name const * g_weak_order = nullptr;
|
||||
name const * g_partial_order = nullptr;
|
||||
name const * g_well_founded_fix = nullptr;
|
||||
name const * g_well_founded_fix_eq = nullptr;
|
||||
name const * g_well_founded_tactics = nullptr;
|
||||
|
|
@ -745,7 +745,7 @@ void initialize_constants() {
|
|||
g_unsafe_monad_from_pure_bind = new name{"unsafe_monad_from_pure_bind"};
|
||||
g_user_attribute = new name{"user_attribute"};
|
||||
g_vm_monitor = new name{"vm_monitor"};
|
||||
g_weak_order = new name{"weak_order"};
|
||||
g_partial_order = new name{"partial_order"};
|
||||
g_well_founded_fix = new name{"well_founded", "fix"};
|
||||
g_well_founded_fix_eq = new name{"well_founded", "fix_eq"};
|
||||
g_well_founded_tactics = new name{"well_founded_tactics"};
|
||||
|
|
@ -1123,7 +1123,7 @@ void finalize_constants() {
|
|||
delete g_unsafe_monad_from_pure_bind;
|
||||
delete g_user_attribute;
|
||||
delete g_vm_monitor;
|
||||
delete g_weak_order;
|
||||
delete g_partial_order;
|
||||
delete g_well_founded_fix;
|
||||
delete g_well_founded_fix_eq;
|
||||
delete g_well_founded_tactics;
|
||||
|
|
@ -1500,7 +1500,7 @@ name const & get_unit_star_name() { return *g_unit_star; }
|
|||
name const & get_unsafe_monad_from_pure_bind_name() { return *g_unsafe_monad_from_pure_bind; }
|
||||
name const & get_user_attribute_name() { return *g_user_attribute; }
|
||||
name const & get_vm_monitor_name() { return *g_vm_monitor; }
|
||||
name const & get_weak_order_name() { return *g_weak_order; }
|
||||
name const & get_partial_order_name() { return *g_partial_order; }
|
||||
name const & get_well_founded_fix_name() { return *g_well_founded_fix; }
|
||||
name const & get_well_founded_fix_eq_name() { return *g_well_founded_fix_eq; }
|
||||
name const & get_well_founded_tactics_name() { return *g_well_founded_tactics; }
|
||||
|
|
|
|||
|
|
@ -370,7 +370,7 @@ name const & get_unit_star_name();
|
|||
name const & get_unsafe_monad_from_pure_bind_name();
|
||||
name const & get_user_attribute_name();
|
||||
name const & get_vm_monitor_name();
|
||||
name const & get_weak_order_name();
|
||||
name const & get_partial_order_name();
|
||||
name const & get_well_founded_fix_name();
|
||||
name const & get_well_founded_fix_eq_name();
|
||||
name const & get_well_founded_tactics_name();
|
||||
|
|
|
|||
|
|
@ -363,7 +363,7 @@ unit.star
|
|||
unsafe_monad_from_pure_bind
|
||||
user_attribute
|
||||
vm_monitor
|
||||
weak_order
|
||||
partial_order
|
||||
well_founded.fix
|
||||
well_founded.fix_eq
|
||||
well_founded_tactics
|
||||
|
|
|
|||
|
|
@ -371,7 +371,7 @@ expr norm_num_context::mk_nonneg_prf(expr const & e) {
|
|||
} else if (is_one(e)) {
|
||||
return mk_app({mk_const(get_zero_le_one_name()), type, mk_lin_ord_semiring()});
|
||||
} else if (is_zero(e)) {
|
||||
return mk_app({mk_const(get_le_refl_name()), type, mk_wk_order(), mk_zero()});
|
||||
return mk_app({mk_const(get_le_refl_name()), type, mk_partial_order(), mk_zero()});
|
||||
} else {
|
||||
throw exception("mk_nonneg_proof called on zero or non_numeral");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@ class norm_num_context {
|
|||
expr mk_field() { return m_ainst.mk_field(); }
|
||||
expr mk_lin_ord_semiring() { return m_ainst.mk_linear_ordered_semiring(); }
|
||||
expr mk_lin_ord_ring() { return m_ainst.mk_linear_ordered_ring(); }
|
||||
expr mk_wk_order() { return m_ainst.mk_weark_order(); }
|
||||
expr mk_partial_order() { return m_ainst.mk_partial_order(); }
|
||||
|
||||
expr mk_num(mpq const & q) { return m_ainst.mk_num(q); }
|
||||
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ begin
|
|||
refl
|
||||
end
|
||||
|
||||
example {α : Type} [weak_order α] (a : α) : a = a :=
|
||||
example {α : Type} [partial_order α] (a : α) : a = a :=
|
||||
begin
|
||||
apply le_antisymm,
|
||||
apply le_refl,
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
{"message":"file invalidated","response":"ok","seq_num":0}
|
||||
{"message":"file invalidated","response":"ok","seq_num":1}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n foo\ntermhas type\n Type"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n foo\ntermhas type\n Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n foo\ntermhas type\n Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n foo\nterm has type\n Type"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n foo\nterm has type\n Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n foo\nterm has type\n Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
|
||||
{"message":"file invalidated","response":"ok","seq_num":2}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n foo\ntermhas type\n Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n foo\nterm has type\n Type"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
|
||||
{"msgs":[],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"invalid declaration, identifier expected"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"invalid declaration, identifier expected"},{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
|
||||
|
|
|
|||
|
|
@ -368,7 +368,7 @@ run_cmd script_check_id `unit.star
|
|||
run_cmd script_check_id `unsafe_monad_from_pure_bind
|
||||
run_cmd script_check_id `user_attribute
|
||||
run_cmd script_check_id `vm_monitor
|
||||
run_cmd script_check_id `weak_order
|
||||
run_cmd script_check_id `partial_order
|
||||
run_cmd script_check_id `well_founded.fix
|
||||
run_cmd script_check_id `well_founded.fix_eq
|
||||
run_cmd script_check_id `well_founded_tactics
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue