max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init): Bool.tt => Bool.true and Bool.ff => Bool.false

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-20 17:17:37 -07:00
parent f8113a01eb
commit 2be87ecd92
42 changed files with 277 additions and 277 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/coe.lean
View file

@ -144,7 +144,7 @@ instance coeToLift {a : Sort u} {b : Sort v} [HasCoeT a b] : HasLiftT a b :=
/- basic coercions -/
instance coeBoolToProp : HasCoe Bool Prop :=
⟨λ y, y = tt⟩
⟨λ y, y = true⟩
/- Tactics such as the simplifier only unfold reducible constants when checking whether two terms are definitionally
equal or a Term is a proposition. The motivation is performance.
@ -152,10 +152,10 @@ instance coeBoolToProp : HasCoe Bool Prop :=
Thus, we mark the following instance as @[reducible], otherwise `simp` will not visit `↑p` when simplifying `↑p -> q`.
-/
@[reducible] instance coeSortBool : HasCoeToSort Bool :=
⟨Prop, λ y, y = tt⟩
⟨Prop, λ y, y = true⟩
instance coeDecidableEq (x : Bool) : Decidable (coe x) :=
show Decidable (x = tt), from decEq x tt
show Decidable (x = true), from decEq x true
instance coeSubtype {a : Sort u} {p : a → Prop} : HasCoe {x // p x} a :=
⟨Subtype.val⟩

4
library/init/control/alternative.lean
View file

@ -30,8 +30,8 @@ if h : p then pure ⟨h⟩ else failure
/- Later we define a coercion from Bool to Prop, but this version will still be useful.
Given (t : tactic Bool), we can write t >>= guardb -/
@[inline] def guardb {f : Type → Type v} [Alternative f] : Bool → f Unit
| tt := pure ()
| ff := failure
| true := pure ()
| false := failure
@[inline] def optional (x : f α) : f (Option α) :=
some <$> x <|> pure none

8
library/init/control/combinators.lean
View file

@ -56,13 +56,13 @@ def List.mfirst {m : Type u → Type v} [Monad m] [Alternative m] {α : Type w}
@[specialize]
def List.mexists {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
| [] := pure ff
| (a::as) := do b ← f a, if b then pure tt else List.mexists as
| [] := pure false
| (a::as) := do b ← f a, if b then pure true else List.mexists as
@[specialize]
def List.mforall {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
| [] := pure tt
| (a::as) := do b ← f a, if b then List.mforall as else pure ff
| [] := pure true
| (a::as) := do b ← f a, if b then List.mforall as else pure false
@[macroInline] def when {m : Type → Type u} [Monad m] (c : Prop) [h : Decidable c] (t : m Unit) : m Unit :=
if c then t else pure ()

2
library/init/control/estate.lean
View file

@ -94,7 +94,7 @@ instance [Inhabited ε] : Inhabited (Estate ε σ α) :=
/-- Alternative orelse operator that allows to select which exception should be used.
The default is to use the first exception since the standard `orelse` uses the second. -/
@[inline] protected def orelse' (x₁ x₂ : Estate ε σ α) (useFirstEx := tt) : Estate ε σ α :=
@[inline] protected def orelse' (x₁ x₂ : Estate ε σ α) (useFirstEx := true) : Estate ε σ α :=
λ r, match x₁ r with
| Result.error e₁ s₁ :=
(match x₂ (resultOk.mk ⟨⟩ s₁) with

6
library/init/control/except.lean
View file

@ -55,8 +55,8 @@ match ma with
| (Except.ok v) := f v
@[inline] protected def toBool {α : Type v} : Except ε α → Bool
| (Except.ok _) := tt
| (Except.error _) := ff
| (Except.ok _) := true
| (Except.error _) := false
@[inline] protected def toOption {α : Type v} : Except ε α → Option α
| (Except.ok a) := some a
@ -130,7 +130,7 @@ catch t₁ $ λ _, t₂
/-- Alternative orelse operator that allows to select which exception should be used.
The default is to use the first exception since the standard `orelse` uses the second. -/
@[inline] def orelse' [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx := tt) : m α :=
@[inline] def orelse' [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx := true) : m α :=
catch t₁ $ λ e₁, catch t₂ $ λ e₂, throw (if useFirstEx then e₁ else e₂)
@[inline] def liftExcept {ε' : Type u} [MonadExcept ε m] [HasLiftT ε' ε] [Monad m] {α : Type v} : Except ε' α → m α

68
library/init/core.lean
View file

@ -286,8 +286,8 @@ structure Psigma {α : Sort u} (β : α → Sort v) :=
mk :: (fst : α) (snd : β fst)
inductive Bool : Type
| ff : Bool
| tt : Bool
| false : Bool
| true : Bool
/- Remark: Subtype must take a Sort instead of Type because of the axiom strongIndefiniteDescription. -/
structure Subtype {α : Sort u} (p : α → Prop) :=
@ -321,7 +321,7 @@ inductive Option (α : Type u)
| some (val : α) : Option
export Option (none some)
export Bool (ff tt)
export Bool (false true)
inductive List (T : Type u)
| nil {} : List
@ -337,7 +337,7 @@ inductive Nat
/- Auxiliary axiom used to implement `sorry`.
TODO: add this theorem on-demand. That is,
we should only add it if after the first error. -/
unsafe axiom sorryAx (α : Sort u) (synthetic := tt) : α
unsafe axiom sorryAx (α : Sort u) (synthetic := true) : α
/- Declare builtin and reserved notation -/
@ -603,25 +603,25 @@ attribute [elabSimple] BinTree.Node BinTree.leaf
/- Boolean operators -/
@[macroInline] def cond {a : Type u} : Bool → a → a → a
| tt x y := x
| ff x y := y
| true x y := x
| false x y := y
@[macroInline] def bor : Bool → Bool → Bool
| tt _ := tt
| ff b := b
| true _ := true
| false b := b
@[macroInline] def band : Bool → Bool → Bool
| ff _ := ff
| tt b := b
| false _ := false
| true b := b
@[macroInline] def bnot : Bool → Bool
| tt := ff
| ff := tt
| true := false
| false := true
@[macroInline] def bxor : Bool → Bool → Bool
| tt ff := tt
| ff tt := tt
| _ _ := ff
| true false := true
| false true := true
| _ _ := false
prefix ! := bnot
infix || := bor
@ -721,13 +721,13 @@ theorem trueNeFalse : ¬True = False :=
neFalseOfSelf trivial
end ne
theorem eqFfOfNeTt : ∀ {b : Bool}, b ≠ tt → b = ff
| tt h := False.elim (h rfl)
| ff h := rfl
theorem eqFfOfNeTt : ∀ {b : Bool}, b ≠ true → b = false
| true h := False.elim (h rfl)
| false h := rfl
theorem eqTtOfNeFf : ∀ {b : Bool}, b ≠ ff → b = tt
| tt h := rfl
| ff h := False.elim (h rfl)
theorem eqTtOfNeFf : ∀ {b : Bool}, b ≠ false → b = true
| true h := rfl
| false h := False.elim (h rfl)
section
variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
@ -1086,14 +1086,14 @@ theorem forallNotOfNotExists {α : Sort u} {p : α → Prop} : ¬(∃ x, p x)
/- Decidable -/
@[macroInline] def Decidable.toBool (p : Prop) [h : Decidable p] : Bool :=
Decidable.casesOn h (λ h₁, Bool.ff) (λ h₂, Bool.tt)
Decidable.casesOn h (λ h₁, false) (λ h₂, true)
export Decidable (isTrue isFalse toBool)
theorem toBoolTrueEqTt (h : Decidable True) : @toBool True h = tt :=
theorem toBoolTrueEqTt (h : Decidable True) : @toBool True h = true :=
Decidable.casesOn h (λ h, False.elim (Iff.mp notTrue h)) (λ _, rfl)
theorem toBoolFalseEqFf (h : Decidable False) : @toBool False h = ff :=
theorem toBoolFalseEqFf (h : Decidable False) : @toBool False h = false :=
Decidable.casesOn h (λ h, rfl) (λ h, False.elim h)
instance : Decidable True :=
@ -1230,24 +1230,24 @@ match decEq a b with
| isTrue h := isFalse $ λ h', absurd h h'
| isFalse h := isTrue h
theorem Bool.ffNeTt (h : ff = tt) : False :=
theorem Bool.falseNeTrue (h : false = true) : False :=
Bool.noConfusion h
def isDecEq {α : Sort u} (p : α → α → Bool) : Prop := ∀ ⦃x y : α⦄, p x y = tt → x = y
def isDecRefl {α : Sort u} (p : α → α → Bool) : Prop := ∀ x, p x x = tt
def isDecEq {α : Sort u} (p : α → α → Bool) : Prop := ∀ ⦃x y : α⦄, p x y = true → x = y
def isDecRefl {α : Sort u} (p : α → α → Bool) : Prop := ∀ x, p x x = true
instance : DecidableEq Bool :=
{decEq := λ a b, match a, b with
| ff, ff := isTrue rfl
| ff, tt := isFalse Bool.ffNeTt
| tt, ff := isFalse (ne.symm Bool.ffNeTt)
| tt, tt := isTrue rfl}
| false, false := isTrue rfl
| false, true := isFalse Bool.falseNeTrue
| true, false := isFalse (ne.symm Bool.falseNeTrue)
| true, true := isTrue rfl}
@[inline]
def decidableEqOfBoolPred {α : Sort u} {p : α → α → Bool} (h₁ : isDecEq p) (h₂ : isDecRefl p) : DecidableEq α :=
{decEq := λ x y : α,
if hp : p x y = tt then isTrue (h₁ hp)
else isFalse (assume hxy : x = y, absurd (h₂ y) (@Eq.recOn _ _ (λ z _, ¬p z y = tt) _ hxy hp))}
if hp : p x y = true then isTrue (h₁ hp)
else isFalse (assume hxy : x = y, absurd (h₂ y) (@Eq.recOn _ _ (λ z _, ¬p z y = true) _ hxy hp))}
theorem decidableEqInlRefl {α : Sort u} [DecidableEq α] (a : α) : decEq a a = isTrue (Eq.refl a) :=
match (decEq a a) with
@ -1414,7 +1414,7 @@ Inhabited.casesOn h (λ b, ⟨λ a, b⟩)
instance pi.Inhabited (α : Sort u) {β : α → Sort v} [Π x, Inhabited (β x)] : Inhabited (Π x, β x) :=
⟨λ a, default (β a)⟩
instance : Inhabited Bool := ⟨ff⟩
instance : Inhabited Bool := ⟨false⟩
instance : Inhabited True := ⟨trivial⟩

18
library/init/data/list/basic.lean
View file

@ -119,9 +119,9 @@ def lengthAux : List α → Nat → Nat
def length (as : List α) : Nat :=
lengthAux as 0
def Empty : List α → Bool
| [] := tt
| (_ :: _) := ff
def empty : List α → Bool
| [] := true
| (_ :: _) := false
open Option Nat
@ -226,10 +226,10 @@ def take : ℕ → List α → List α
| (a :: l) := some $ foldr1 f (a :: l) (λ Eq, List.noConfusion Eq)
@[inline] def any (l : List α) (p : α → Bool) : Bool :=
foldr (λ a r, p a || r) ff l
foldr (λ a r, p a || r) false l
@[inline] def all (l : List α) (p : α → Bool) : Bool :=
foldr (λ a r, p a && r) tt l
foldr (λ a r, p a && r) true l
def bor (l : List Bool) : Bool := any l id
@ -355,13 +355,13 @@ lemma ltEqNotGe [HasLt α] [decidableRel ((<) : α → α → Prop)] : ∀ l₁
show (l₁ < l₂) = ¬ ¬ (l₁ < l₂), from
Eq.subst (propext (notNotIff (l₁ < l₂))).symm rfl
/-- `isPrefixOf l₁ l₂` returns `tt` Iff `l₁` is a prefix of `l₂`. -/
/-- `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/
def isPrefixOf [DecidableEq α] : List α → List α → Bool
| [] _ := tt
| _ [] := ff
| [] _ := true
| _ [] := false
| (a::as) (b::bs) := toBool (a = b) && isPrefixOf as bs
/-- `isSuffixOf l₁ l₂` returns `tt` Iff `l₁` is a suffix of `l₂`. -/
/-- `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`. -/
def isSuffixOf [DecidableEq α] (l₁ l₂ : List α) : Bool :=
isPrefixOf l₁.reverse l₂.reverse

26
library/init/data/nat/basic.lean
View file

@ -13,32 +13,32 @@ namespace Nat
@[extern cpp "lean::nat_dec_eq"]
def beq : Nat → Nat → Bool
| zero zero := tt
| zero (succ m) := ff
| (succ n) zero := ff
| zero zero := true
| zero (succ m) := false
| (succ n) zero := false
| (succ n) (succ m) := beq n m
theorem eqOfBeqEqTt : ∀ {n m : Nat}, beq n m = tt → n = m
theorem eqOfBeqEqTt : ∀ {n m : Nat}, beq n m = true → n = m
| zero zero h := rfl
| zero (succ m) h := Bool.noConfusion h
| (succ n) zero h := Bool.noConfusion h
| (succ n) (succ m) h :=
have beq n m = tt, from h,
have beq n m = true, from h,
have n = m, from eqOfBeqEqTt this,
congrArg succ this
theorem neOfBeqEqFf : ∀ {n m : Nat}, beq n m = ff → n ≠ m
theorem neOfBeqEqFf : ∀ {n m : Nat}, beq n m = false → n ≠ m
| zero zero h₁ h₂ := Bool.noConfusion h₁
| zero (succ m) h₁ h₂ := Nat.noConfusion h₂
| (succ n) zero h₁ h₂ := Nat.noConfusion h₂
| (succ n) (succ m) h₁ h₂ :=
have beq n m = ff, from h₁,
have beq n m = false, from h₁,
have n ≠ m, from neOfBeqEqFf this,
Nat.noConfusion h₂ (λ h₂, absurd h₂ this)
@[extern cpp "lean::nat_dec_eq"]
protected def decEq (n m : @& Nat) : Decidable (n = m) :=
if h : beq n m = tt then isTrue (eqOfBeqEqTt h)
if h : beq n m = true then isTrue (eqOfBeqEqTt h)
else isFalse (neOfBeqEqFf (eqFfOfNeTt h))
@[inline] instance : DecidableEq Nat :=
@ -46,13 +46,13 @@ else isFalse (neOfBeqEqFf (eqFfOfNeTt h))
@[extern cpp "lean::nat_dec_le"]
def ble : Nat → Nat → Bool
| zero zero := tt
| zero (succ m) := tt
| (succ n) zero := ff
| zero zero := true
| zero (succ m) := true
| (succ n) zero := false
| (succ n) (succ m) := ble n m
protected def le (n m : Nat) : Prop :=
ble n m = tt
ble n m = true
instance : HasLe Nat :=
⟨Nat.le⟩
@ -261,7 +261,7 @@ predLePred
@[extern cpp "lean::nat_dec_le"]
instance decLe (n m : @& Nat) : Decidable (n ≤ m) :=
decEq (ble n m) tt
decEq (ble n m) true
@[extern cpp "lean::nat_dec_lt"]
instance decLt (n m : @& Nat) : Decidable (n < m) :=

4
library/init/data/nat/bitwise.lean
View file

@ -8,8 +8,8 @@ import init.data.nat.basic init.data.nat.div init.coe
namespace Nat
def bitwise (f : Bool → Bool → Bool) : Nat → Nat → Nat | n m :=
if n = 0 then (if f ff tt then m else 0)
else if m = 0 then (if f tt ff then n else 0)
if n = 0 then (if f false true then m else 0)
else if m = 0 then (if f true false then n else 0)
else
let n' := n / 2 in
let m' := m / 2 in

12
library/init/data/option/basic.lean
View file

@ -24,16 +24,16 @@ def get {α : Type u} [Inhabited α] : Option α → α
| none := default α
def toBool {α : Type u} : Option α → Bool
| (some _) := tt
| none := ff
| (some _) := true
| none := false
def isSome {α : Type u} : Option α → Bool
| (some _) := tt
| none := ff
| (some _) := true
| none := false
def isNone {α : Type u} : Option α → Bool
| (some _) := ff
| none := tt
| (some _) := false
| none := true
@[inline] protected def bind {α : Type u} {β : Type v} : Option α → (α → Option β) → Option β
| none b := none

12
library/init/data/rbmap/basic.lean
View file

@ -47,11 +47,11 @@ protected def max : Rbnode α β → Option (Σ k : α, β k)
| (Node _ l k v r) b := revFold l (f k v (revFold r b))
@[specialize] def all (p : Π k : α, β k → Bool) : Rbnode α β → Bool
| leaf := tt
| leaf := true
| (Node _ l k v r) := p k v && all l && all r
@[specialize] def any (p : Π k : α, β k → Bool) : Rbnode α β → Bool
| leaf := ff
| leaf := false
| (Node _ l k v r) := p k v || any l || any r
def balance1 : Rbnode α β → Rbnode α β → Rbnode α β
@ -67,8 +67,8 @@ def balance2 : Rbnode α β → Rbnode α β → Rbnode α β
| _ _ := leaf -- unreachable
def isRed : Rbnode α β → Bool
| (Node red _ _ _ _) := tt
| _ := ff
| (Node red _ _ _ _) := true
| _ := false
section insert
@ -167,8 +167,8 @@ t.val.depth f
t.mfold (λ k v _, f k v *> pure ⟨⟩) ⟨⟩
@[inline] def Empty : Rbmap α β lt → Bool
| ⟨leaf, _⟩ := tt
| _ := ff
| ⟨leaf, _⟩ := true
| _ := false
@[specialize] def toList : Rbmap α β lt → List (α × β)
| ⟨t, _⟩ := t.revFold (λ k v ps, (k, v)::ps) []

14
library/init/data/repr.lean
View file

@ -19,19 +19,19 @@ instance {α : Type u} [HasRepr α] : HasRepr (id α) :=
inferInstanceAs (HasRepr α)
instance : HasRepr Bool :=
⟨λ b, cond b "tt" "ff"⟩
⟨λ b, cond b "true" "false"⟩
instance {p : Prop} : HasRepr (Decidable p) :=
⟨λ b : Decidable p, @ite p b _ "tt" "ff"⟩
⟨λ b : Decidable p, @ite p b _ "true" "false"⟩
protected def List.reprAux {α : Type u} [HasRepr α] : Bool → List α → String
| b [] := ""
| tt (x::xs) := repr x ++ List.reprAux ff xs
| ff (x::xs) := ", " ++ repr x ++ List.reprAux ff xs
| b [] := ""
| true (x::xs) := repr x ++ List.reprAux false xs
| false (x::xs) := ", " ++ repr x ++ List.reprAux false xs
protected def List.repr {α : Type u} [HasRepr α] : List α → String
| [] := "[]"
| (x::xs) := "[" ++ List.reprAux tt (x::xs) ++ "]"
| (x::xs) := "[" ++ List.reprAux true (x::xs) ++ "]"
instance {α : Type u} [HasRepr α] : HasRepr (List α) :=
⟨List.repr⟩
@ -119,7 +119,7 @@ def String.quoteAux : List Char → String
| (x::xs) := Char.quoteCore x ++ String.quoteAux xs
def String.quote (s : String) : String :=
if s.isEmpty = tt then "\"\""
if s.isEmpty = true then "\"\""
else "\"" ++ String.quoteAux s.toList ++ "\""
instance : HasRepr String :=

4
library/init/data/string/basic.lean
View file

@ -214,7 +214,7 @@ def forward : Iterator → Nat → Iterator
def remainingToString : Iterator → String
| ⟨s, _, i⟩ := s.extract i s.bsize
/- (isPrefixOfRemaining it₁ it₂) is `tt` Iff `it₁.remainingToString` is a prefix
/- (isPrefixOfRemaining it₁ it₂) is `true` Iff `it₁.remainingToString` is a prefix
of `it₂.remainingToString`. -/
def isPrefixOfRemaining : Iterator → Iterator → Bool
| ⟨s₁, _, i₁⟩ ⟨s₂, _, i₂⟩ := s₁.extract i₁ s₁.bsize = s₂.extract i₂ (i₂ + (s₁.bsize - i₁))
@ -264,7 +264,7 @@ end Iterator
private def lineColumnAux : Nat → String.Iterator → Nat × Nat → Nat × Nat
| 0 it r := r
| (k+1) it r@(line, col) :=
if it.hasNext = ff then r
if it.hasNext = false then r
else match it.curr with
| '\n' := lineColumnAux k it.next (line+1, 0)
| other := lineColumnAux k it.next (line, col+1)

12
library/init/data/tostring.lean
View file

@ -25,20 +25,20 @@ instance : HasToString String.Iterator :=
⟨λ it, it.remainingToString⟩
instance : HasToString Bool :=
⟨λ b, cond b "tt" "ff"⟩
⟨λ b, cond b "true" "false"⟩
instance {p : Prop} : HasToString (Decidable p) :=
-- Remark: type class inference will not consider local instance `b` in the new Elaborator
⟨λ b : Decidable p, @ite p b _ "tt" "ff"⟩
⟨λ b : Decidable p, @ite p b _ "true" "false"⟩
protected def List.toStringAux {α : Type u} [HasToString α] : Bool → List α → String
| b [] := ""
| tt (x::xs) := toString x ++ List.toStringAux ff xs
| ff (x::xs) := ", " ++ toString x ++ List.toStringAux ff xs
| b [] := ""
| true (x::xs) := toString x ++ List.toStringAux false xs
| false (x::xs) := ", " ++ toString x ++ List.toStringAux false xs
protected def List.toString {α : Type u} [HasToString α] : List α → String
| [] := "[]"
| (x::xs) := "[" ++ List.toStringAux tt (x::xs) ++ "]"
| (x::xs) := "[" ++ List.toStringAux true (x::xs) ++ "]"
instance {α : Type u} [HasToString α] : HasToString (List α) :=
⟨List.toString⟩

8
library/init/io.lean
View file

@ -76,7 +76,7 @@ constant putStr (s: @& String) : IO Unit := default _
@[extern 1 "lean_io_prim_get_line"]
constant getLine : IO String := default _
@[extern 4 "lean_io_prim_handle_mk"]
constant handle.mk (s : @& String) (m : Mode) (bin : Bool := ff) : IO handle := default _
constant handle.mk (s : @& String) (m : Mode) (bin : Bool := false) : IO handle := default _
@[extern 2 "lean_io_prim_handle_is_eof"]
constant handle.isEof (h : @& handle) : IO Bool := default _
@[extern 2 "lean_io_prim_handle_flush"]
@ -109,7 +109,7 @@ end
namespace Fs
variables {m : Type → Type} [Monad m] [monadIO m]
def handle.mk (s : String) (Mode : Mode) (bin : Bool := ff) : m handle := Prim.liftIO (Prim.handle.mk s Mode bin)
def handle.mk (s : String) (Mode : Mode) (bin : Bool := false) : m handle := Prim.liftIO (Prim.handle.mk s Mode bin)
def handle.isEof : handle → m Bool := Prim.liftIO ∘ Prim.handle.isEof
def handle.flush : handle → m Unit := Prim.liftIO ∘ Prim.handle.flush
def handle.close : handle → m Unit := Prim.liftIO ∘ Prim.handle.flush
@ -143,13 +143,13 @@ Prim.liftIO $ Prim.iterate "" $ λ r, do
c ← h.getLine,
pure $ Sum.inl (r ++ c) -- continue
def readFile (fname : String) (bin := ff) : m String :=
def readFile (fname : String) (bin := false) : m String :=
do h ← handle.mk fname Mode.read bin,
r ← h.readToEnd,
h.close,
pure r
-- def writeFile (fname : String) (data : String) (bin := ff) : m Unit :=
-- def writeFile (fname : String) (data : String) (bin := false) : m Unit :=
-- do h ← handle.mk fname Mode.write bin,
-- h.write data,
-- h.close

8
library/init/lean/compiler/constfolding.lean
View file

@ -93,10 +93,10 @@ mkBinApp (mkBinApp (Expr.const `HasLt.le [Level.zero]) (Expr.const `Nat []) (Exp
def toDecidableExpr (beforeErasure : Bool) (pred : Expr) (r : Bool) : Expr :=
match beforeErasure, r with
| ff, tt := mkDecIsTrue neutralExpr neutralExpr
| ff, ff := mkDecIsFalse neutralExpr neutralExpr
| tt, tt := mkDecIsTrue pred (mkLcProof pred)
| tt, ff := mkDecIsFalse pred (mkLcProof pred)
| false, true := mkDecIsTrue neutralExpr neutralExpr
| false, false := mkDecIsFalse neutralExpr neutralExpr
| true, true := mkDecIsTrue pred (mkLcProof pred)
| true, false := mkDecIsFalse pred (mkLcProof pred)
def foldNatBinPred (mkPred : Expr → Expr → Expr) (fn : Nat → Nat → Bool)
(beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr :=

82
library/init/lean/compiler/ir.lean
View file

@ -46,16 +46,16 @@ inductive IRType
| irrelevant | object | tobject
def IRType.beq : IRType → IRType → Bool
| IRType.float IRType.float := tt
| IRType.Uint8 IRType.Uint8 := tt
| IRType.Uint16 IRType.Uint16 := tt
| IRType.Uint32 IRType.Uint32 := tt
| IRType.Uint64 IRType.Uint64 := tt
| IRType.Usize IRType.Usize := tt
| IRType.irrelevant IRType.irrelevant := tt
| IRType.object IRType.object := tt
| IRType.tobject IRType.tobject := tt
| _ _ := ff
| IRType.float IRType.float := true
| IRType.Uint8 IRType.Uint8 := true
| IRType.Uint16 IRType.Uint16 := true
| IRType.Uint32 IRType.Uint32 := true
| IRType.Uint64 IRType.Uint64 := true
| IRType.Usize IRType.Usize := true
| IRType.irrelevant IRType.irrelevant := true
| IRType.object IRType.object := true
| IRType.tobject IRType.tobject := true
| _ _ := false
instance IRType.HasBeq : HasBeq IRType := ⟨IRType.beq⟩
@ -74,7 +74,7 @@ inductive Litval
def Litval.beq : Litval → Litval → Bool
| (Litval.num v₁) (Litval.num v₂) := v₁ = v₂
| (Litval.str v₁) (Litval.str v₂) := v₁ = v₂
| _ _ := ff
| _ _ := false
instance Litval.HasBeq : HasBeq Litval := ⟨Litval.beq⟩
@ -146,9 +146,9 @@ inductive Fnbody
`ty` must not be `object`, `tobject`, `irrelevant` nor `Usize`. -/
| sset (x : varid) (i : Nat) (offset : Nat) (y : varid) (ty : IRType) (b : Fnbody)
| release (x : varid) (i : Nat) (b : Fnbody)
/- RC increment for `object`. If c = `tt`, then `inc` must check whether `x` is a tagged pointer or not. -/
/- RC increment for `object`. If c = `true`, then `inc` must check whether `x` is a tagged pointer or not. -/
| inc (x : varid) (n : Nat) (c : Bool) (b : Fnbody)
/- RC decrement for `object`. If c = `tt`, then `inc` must check whether `x` is a tagged pointer or not. -/
/- RC decrement for `object`. If c = `true`, then `inc` must check whether `x` is a tagged pointer or not. -/
| dec (x : varid) (n : Nat) (c : Bool) (b : Fnbody)
| mdata (d : Kvmap) (b : Fnbody)
| case (tid : Name) (x : varid) (cs : List (AltCore Fnbody))
@ -165,19 +165,19 @@ inductive Decl
| fdecl (f : fid) (xs : List Param) (ty : IRType) (b : Fnbody)
| extern (f : fid) (xs : List Param) (ty : IRType)
/-- `Expr.isPure e` return `tt` Iff `e` is in the `λPure` fragment. -/
/-- `Expr.isPure e` return `true` Iff `e` is in the `λPure` fragment. -/
def Expr.isPure : Expr → Bool
| (Expr.ctor _ _) := tt
| (Expr.proj _ _) := tt
| (Expr.uproj _ _) := tt
| (Expr.sproj _ _) := tt
| (Expr.fap _ _) := tt
| (Expr.pap _ _) := tt
| (Expr.ap _ _) := tt
| (Expr.lit _) := tt
| _ := ff
| (Expr.ctor _ _) := true
| (Expr.proj _ _) := true
| (Expr.uproj _ _) := true
| (Expr.sproj _ _) := true
| (Expr.fap _ _) := true
| (Expr.pap _ _) := true
| (Expr.ap _ _) := true
| (Expr.lit _) := true
| _ := false
/-- `Fnbody.isPure b` return `tt` Iff `b` is in the `λPure` fragment. -/
/-- `Fnbody.isPure b` return `true` Iff `b` is in the `λPure` fragment. -/
mutual def Fnbody.isPure, alts.isPure, alt.isPure
with Fnbody.isPure : Fnbody → Bool
| (Fnbody.vdecl _ _ e b) := e.isPure && b.isPure
@ -186,16 +186,16 @@ with Fnbody.isPure : Fnbody → Bool
| (Fnbody.sset _ _ _ _ _ b) := b.isPure
| (Fnbody.mdata _ b) := b.isPure
| (Fnbody.case _ _ cs) := alts.isPure cs
| (Fnbody.ret _) := tt
| (Fnbody.jmp _ _) := tt
| Fnbody.unreachable := tt
| _ := ff
| (Fnbody.ret _) := true
| (Fnbody.jmp _ _) := true
| Fnbody.unreachable := true
| _ := false
with alts.isPure : List alt → Bool
| [] := tt
| [] := true
| (a::as) := a.isPure && alts.isPure as
with alt.isPure : alt → Bool
| (alt.ctor _ b) := b.isPure
| (alt.default b) := ff
| (alt.default b) := false
abbrev varRenaming := NameMap Name
@ -213,15 +213,15 @@ instance varid.hasAeqv : HasAlphaEqv varid := ⟨varid.alphaEqv⟩
def Arg.alphaEqv (ρ : varRenaming) : Arg → Arg → Bool
| (Arg.var v₁) (Arg.var v₂) := v₁ =[ρ]= v₂
| Arg.irrelevant Arg.irrelevant := tt
| _ _ := ff
| Arg.irrelevant Arg.irrelevant := true
| _ _ := false
instance Arg.hasAeqv : HasAlphaEqv Arg := ⟨Arg.alphaEqv⟩
def args.alphaEqv (ρ : varRenaming) : List Arg → List Arg → Bool
| [] [] := tt
| [] [] := true
| (a::as) (b::bs) := a =[ρ]= b && args.alphaEqv as bs
| _ _ := ff
| _ _ := false
instance args.hasAeqv : HasAlphaEqv (List Arg) := ⟨args.alphaEqv⟩
@ -240,7 +240,7 @@ def Expr.alphaEqv (ρ : varRenaming) : Expr → Expr → Bool
| (Expr.lit v₁) (Expr.lit v₂) := v₁ == v₂
| (Expr.isShared x₁) (Expr.isShared x₂) := x₁ =[ρ]= x₂
| (Expr.isTaggedPtr x₁) (Expr.isTaggedPtr x₂) := x₁ =[ρ]= x₂
| _ _ := ff
| _ _ := false
instance Expr.hasAeqv : HasAlphaEqv Expr:= ⟨Expr.alphaEqv⟩
@ -262,7 +262,7 @@ with Fnbody.alphaEqv : varRenaming → Fnbody → Fnbody → Bool
| ρ (Fnbody.jdecl j₁ ys₁ t₁ v₁ b₁) (Fnbody.jdecl j₂ ys₂ t₂ v₂ b₂) :=
(match addParamsRename ρ ys₁ ys₂ with
| some ρ' := t₁ == t₂ && Fnbody.alphaEqv ρ' v₁ v₂ && Fnbody.alphaEqv (addVarRename ρ j₁ j₂) b₁ b₂
| none := ff)
| none := false)
| ρ (Fnbody.set x₁ i₁ y₁ b₁) (Fnbody.set x₂ i₂ y₂ b₂) := x₁ =[ρ]= x₂ && i₁ = i₂ && y₁ =[ρ]= y₂ && Fnbody.alphaEqv ρ b₁ b₂
| ρ (Fnbody.uset x₁ i₁ y₁ b₁) (Fnbody.uset x₂ i₂ y₂ b₂) := x₁ =[ρ]= x₂ && i₁ = i₂ && y₁ =[ρ]= y₂ && Fnbody.alphaEqv ρ b₁ b₂
| ρ (Fnbody.sset x₁ i₁ o₁ y₁ t₁ b₁) (Fnbody.sset x₂ i₂ o₂ y₂ t₂ b₂) :=
@ -274,16 +274,16 @@ with Fnbody.alphaEqv : varRenaming → Fnbody → Fnbody → Bool
| ρ (Fnbody.case n₁ x₁ as₁) (Fnbody.case n₂ x₂ as₂) := n₁ = n₂ && x₁ =[ρ]= x₂ && alts.alphaEqv ρ as₁ as₂
| ρ (Fnbody.jmp j₁ ys₁) (Fnbody.jmp j₂ ys₂) := j₁ = j₂ && ys₁ =[ρ]= ys₂
| ρ (Fnbody.ret x₁) (Fnbody.ret x₂) := x₁ =[ρ]= x₂
| _ Fnbody.unreachable Fnbody.unreachable := tt
| _ _ _ := ff
| _ Fnbody.unreachable Fnbody.unreachable := true
| _ _ _ := false
with alts.alphaEqv : varRenaming → List alt → List alt → Bool
| _ [] [] := tt
| _ [] [] := true
| ρ (a₁::as₁) (a₂::as₂) := alt.alphaEqv ρ a₁ a₂ && alts.alphaEqv ρ as₁ as₂
| _ _ _ := ff
| _ _ _ := false
with alt.alphaEqv : varRenaming → alt → alt → Bool
| ρ (alt.ctor i₁ b₁) (alt.ctor i₂ b₂) := i₁ == i₂ && Fnbody.alphaEqv ρ b₁ b₂
| ρ (alt.default b₁) (alt.default b₂) := Fnbody.alphaEqv ρ b₁ b₂
| _ _ _ := ff
| _ _ _ := false
def Fnbody.beq (b₁ b₂ : Fnbody) : Bool :=
Fnbody.alphaEqv mkNameMap b₁ b₂

2
library/init/lean/declaration.lean
View file

@ -84,7 +84,7 @@ structure inductiveVal extends ConstantVal :=
(nindices : Nat) -- Number of indices
(all : List Name) -- List of all (including this one) inductive datatypes in the mutual Declaration containing this one
(cnstrs : List Name) -- List of all constructors for this inductive datatype
(isRec : Bool) -- `tt` Iff it is recursive
(isRec : Bool) -- `true` Iff it is recursive
(isUnsafe : Bool)
(isReflexive : Bool)

42
library/init/lean/elaborator.lean
View file

@ -16,7 +16,7 @@ namespace Lean
constant environment : Type := Unit
@[extern "lean_environment_contains"]
constant environment.contains (env : @& environment) (n : @& Name) : Bool := ff
constant environment.contains (env : @& environment) (n : @& Name) : Bool := false
-- deprecated Constructor
@[extern "lean_expr_local"]
constant Expr.local (n : Name) (pp : Name) (ty : Expr) (bi : BinderInfo) : Expr := default Expr
@ -287,14 +287,14 @@ def toPexpr : Syntax → ElaboratorM Expr
let v := view structInst stx,
-- order should be: fields*, sources*, catchall?
let (fields, other) := v.items.span (λ it, ↑match SepBy.Elem.View.item it with
| structInstItem.View.field _ := tt
| _ := ff),
| structInstItem.View.field _ := true
| _ := false),
let (sources, catchall) := other.span (λ it, ↑match SepBy.Elem.View.item it with
| structInstItem.View.source {source := some _} := tt
| _ := ff),
| structInstItem.View.source {source := some _} := true
| _ := false),
catchall ← match catchall with
| [] := pure ff
| [{item := structInstItem.View.source _}] := pure tt
| [] := pure false
| [{item := structInstItem.View.source _}] := pure true
| {item := it}::_ := error (review structInstItem it) $ "unexpected item in structure instance notation",
fields ← fields.mmap (λ f, match SepBy.Elem.View.item f with
@ -325,7 +325,7 @@ def toPexpr : Syntax → ElaboratorM Expr
let eqns := mkEqns type eqns,
Expr.mdata mdata e ← pure eqns
| error stx "toPexpr: unreachable",
let eqns := Expr.mdata (mdata.setBool `match tt) e,
let eqns := Expr.mdata (mdata.setBool `match true) e,
Expr.mkApp eqns <$> v.scrutinees.mmap (λ scr, toPexpr scr.item)
| _ := error stx $ "toPexpr: unexpected Node: " ++ toString k.name,
(match k with
@ -386,8 +386,8 @@ def declModifiersToPexpr (mods : declModifiers.View) : ElaboratorM Expr := do
| some {doc := some doc, ..} := mdata.setString `docString doc.val
| _ := mdata,
let mdata := match mods.visibility with
| some (visibility.View.private _) := mdata.setBool `private tt
| some (visibility.View.protected _) := mdata.setBool `protected tt
| some (visibility.View.private _) := mdata.setBool `private true
| some (visibility.View.protected _) := mdata.setBool `protected true
| _ := mdata,
let mdata := mdata.setBool `noncomputable mods.noncomputable.isSome,
let mdata := mdata.setBool `unsafe mods.unsafe.isSome,
@ -587,8 +587,8 @@ def variables.elaborate : Elaborator :=
modifyCurrentScope $ λ sc, {sc with vars :=
sc.vars.insert id {v with BinderInfo := bi}}
| none := error (Syntax.ident id) "",
pure ff
else pure tt
pure false
else pure true
| _ := error stx "variables.elaborate: unexpected input",
vars ← simpleBindersToPexpr vars,
oldElabCommand stx $ Expr.mdata mdata vars
@ -705,9 +705,9 @@ def reserveNotation.elaborate : Elaborator :=
updateParserConfig
def matchPrecedence : Option precedence.View → Option precedence.View → Bool
| none (some rp) := tt
| none (some rp) := true
| (some sp) (some rp) := sp.Term.toNat = rp.Term.toNat
| _ _ := ff
| _ _ := false
/-- Check if a notation is compatible with a reserved notation, and if so, copy missing
precedences in the notation from the reserved notation. -/
@ -774,8 +774,8 @@ def notation.elaborate : Elaborator :=
let nota := view «notation» stx,
-- HACK: ignore List Literal notation using :fold
let usesFold := nota.spec.rules.any $ λ r, match r.transition with
| some (transition.View.Arg {action := some {kind := actionKind.View.fold _, ..}, ..}) := tt
| _ := ff,
| some (transition.View.Arg {action := some {kind := actionKind.View.fold _, ..}, ..}) := true
| _ := false,
if usesFold then do {
cfg ← read,
modify $ λ st, {st with messages := st.messages.add {filename := cfg.filename, pos := ⟨1,0⟩,
@ -842,7 +842,7 @@ def setOption.elaborate : Elaborator :=
let opts := sc.Options,
-- TODO(Sebastian): check registered Options
let opts := match v.val with
| optionValue.View.Bool b := opts.setBool opt (match b with boolOptionValue.View.True _ := tt | _ := ff)
| optionValue.View.Bool b := opts.setBool opt (match b with boolOptionValue.View.True _ := true | _ := false)
| optionValue.View.String lit := (match lit.value with
| some s := opts.setString opt s
| none := opts) -- Parser already failed
@ -917,19 +917,19 @@ def elaborators : Rbmap Name Elaborator (<) := Rbmap.fromList [
-- TODO: optimize
def isOpenNamespace (sc : Scope) : Name → Bool
| Name.anonymous := tt
| Name.anonymous := true
| ns :=
-- check surrounding namespaces
ns ∈ sc.nsStack ∨
-- check opened namespaces
sc.openDecls.any (λ od, od.id.val = ns) ∨
-- TODO: check active exports
ff
false
-- TODO: `hiding`, `as`, `renaming`
def matchOpenSpec (n : Name) (spec : openSpec.View) : Option Name :=
let matchesOnly := match spec.only with
| none := tt
| none := true
| some only := n = only.id.val ∨ only.ids.any (λ id, n = id.val) in
if matchesOnly then some (spec.id.val ++ n) else none
@ -954,7 +954,7 @@ def resolveContext : Name → ElaboratorM (List Name)
-- check environment directly
(let unrooted := n.replacePrefix `_root_ Name.anonymous in
match st.env.contains unrooted with
| tt := [unrooted]
| true := [unrooted]
| _ := [])
++
-- check opened namespaces

2
library/init/lean/expander.lean
View file

@ -466,7 +466,7 @@ def universes.transform : transformer :=
pure $ Syntax.list $ v.ids.map (λ id, review «universe» {id := id})
def sorry.transform : transformer :=
λ stx, pure $ mkApp (globId `sorryAx) [review hole {}, globId `Bool.ff]
λ stx, pure $ mkApp (globId `sorryAx) [review hole {}, globId `Bool.false]
local attribute [instance] Name.hasLtQuick

30
library/init/lean/format.lean
View file

@ -18,30 +18,30 @@ inductive Format
| choice : Format → Format → Format
namespace Format
instance : HasAppend Format := ⟨compose ff⟩
instance : HasAppend Format := ⟨compose false⟩
instance : HasCoe String Format := ⟨text⟩
def join (xs : List Format) : Format :=
xs.foldl (++) ""
def flatten : Format → Format
| nil := nil
| line := text " "
| f@(text _) := f
| (nest _ f) := flatten f
| (choice f _) := flatten f
| f@(compose tt _ _) := f
| f@(compose ff f₁ f₂) := compose tt (flatten f₁) (flatten f₂)
| nil := nil
| line := text " "
| f@(text _) := f
| (nest _ f) := flatten f
| (choice f _) := flatten f
| f@(compose true _ _) := f
| f@(compose false f₁ f₂) := compose true (flatten f₁) (flatten f₂)
def group : Format → Format
| nil := nil
| f@(text _) := f
| f@(compose tt _ _) := f
| f := choice (flatten f) f
| nil := nil
| f@(text _) := f
| f@(compose true _ _) := f
| f := choice (flatten f) f
structure SpaceResult :=
(found := ff)
(exceeded := ff)
(found := false)
(exceeded := false)
(space := 0)
/-
@ -56,7 +56,7 @@ else let y := r₂.get in
def spaceUptoLine : Format → Nat → SpaceResult
| nil w := {}
| line w := { found := tt }
| line w := { found := true }
| (text s) w := { space := s.length, exceeded := s.length > w }
| (compose _ f₁ f₂) w := merge w (spaceUptoLine f₁ w) (spaceUptoLine f₂ w)
| (nest _ f) w := spaceUptoLine f w

4
library/init/lean/frontend.lean
View file

@ -35,7 +35,7 @@ def runFrontend (filename input : String) (printMsg : Message → IO Unit) (coll
msgs.toList.mfor printMsg,
let expanderCfg : ExpanderConfig := {transformers := builtinTransformers, ..parserCfg},
let elabCfg : ElaboratorConfig := {filename := filename, input := input, initialParserCfg := parserCfg, ..parserCfg},
let opts := Options.mk.setBool `Trace.asMessages tt,
let opts := Options.mk.setBool `Trace.asMessages true,
let elabSt := Elaborator.mkState elabCfg env opts,
let addOutput (out : Syntax) outs := if collectOutputs then out::outs else [],
IO.Prim.iterate (pSnap, elabSt, parserCfg, expanderCfg, ([] : List Syntax)) $ λ ⟨pSnap, elabSt, parserCfg, expanderCfg, outs⟩, do {
@ -84,7 +84,7 @@ def processFile (f s : String) (json : Bool) : StateT environment IO Unit := do
else IO.println msg.toString,
-- print and erase uncaught exceptions
catch
(runFrontend f s printMsg ff *> pure ())
(runFrontend f s printMsg false *> pure ())
(λ e, do
monadLift (printMsg {filename := f, severity := MessageSeverity.error, pos := ⟨1, 0⟩, text := e}),
throw e)

6
library/init/lean/kvmap.lean
View file

@ -18,7 +18,7 @@ def DataValue.beq : DataValue → DataValue → Bool
| (DataValue.ofString s₁) (DataValue.ofString s₂) := s₁ = s₂
| (DataValue.ofNat n₁) (DataValue.ofNat n₂) := n₂ = n₂
| (DataValue.ofBool b₁) (DataValue.ofBool b₂) := b₁ = b₂
| _ _ := ff
| _ _ := false
instance DataValue.HasBeq : HasBeq DataValue := ⟨DataValue.beq⟩
@ -79,11 +79,11 @@ def setName (m : Kvmap) (k : Name) (v : Name) : Kvmap :=
m.insert k (DataValue.ofName v)
def subset : Kvmap → Kvmap → Bool
| ⟨[]⟩ m₂ := tt
| ⟨[]⟩ m₂ := true
| ⟨(k, v₁)::m₁⟩ m₂ :=
(match m₂.find k with
| some v₂ := v₁ == v₂ && subset ⟨m₁⟩ m₂
| none := ff)
| none := false)
def eqv (m₁ m₂ : Kvmap) : Bool :=
subset m₁ m₂ && subset m₂ m₁

18
library/init/lean/level.lean
View file

@ -28,18 +28,18 @@ instance levelIsInhabited : Inhabited Level :=
def Level.one : Level := Level.succ Level.zero
def Level.hasParam : Level → Bool
| (Level.Param _) := tt
| (Level.Param _) := true
| (Level.succ l) := Level.hasParam l
| (Level.max l₁ l₂) := Level.hasParam l₁ || Level.hasParam l₂
| (Level.imax l₁ l₂) := Level.hasParam l₁ || Level.hasParam l₂
| _ := ff
| _ := false
def Level.hasMvar : Level → Bool
| (Level.mvar _) := tt
| (Level.mvar _) := true
| (Level.succ l) := Level.hasParam l
| (Level.max l₁ l₂) := Level.hasParam l₁ || Level.hasParam l₂
| (Level.imax l₁ l₂) := Level.hasParam l₁ || Level.hasParam l₂
| _ := ff
| _ := false
def Level.ofNat : Nat → Level
| 0 := Level.zero
@ -97,8 +97,8 @@ def Result.imax : Result → Result → Result
| f₁ f₂ := Result.imaxNode [f₁, f₂]
def parenIfFalse : Format → Bool → Format
| f tt := f
| f ff := f.paren
| f true := f
| f false := f.paren
mutual def Result.toFormat, resultList.toFormat
with Result.toFormat : Result → Bool → Format
@ -106,13 +106,13 @@ with Result.toFormat : Result → Bool → Format
| (Result.num k) _ := toString k
| (Result.offset f 0) r := Result.toFormat f r
| (Result.offset f (k+1)) r :=
let f' := Result.toFormat f ff in
let f' := Result.toFormat f false in
parenIfFalse (f' ++ "+" ++ toFmt (k+1)) r
| (Result.maxNode Fs) r := parenIfFalse (Format.group $ "max" ++ resultList.toFormat Fs) r
| (Result.imaxNode Fs) r := parenIfFalse (Format.group $ "imax" ++ resultList.toFormat Fs) r
with resultList.toFormat : List Result → Format
| [] := Format.nil
| (r::rs) := Format.line ++ Result.toFormat r ff ++ resultList.toFormat rs
| (r::rs) := Format.line ++ Result.toFormat r false ++ resultList.toFormat rs
def Level.toResult : Level → Result
| Level.zero := Result.num 0
@ -123,7 +123,7 @@ def Level.toResult : Level → Result
| (Level.mvar n) := Result.leaf (toFmt n)
def Level.toFormat (l : Level) : Format :=
(Level.toResult l).toFormat tt
(Level.toResult l).toFormat true
instance levelHasToFormat : HasToFormat Level := ⟨Level.toFormat⟩
instance levelHasToString : HasToString Level := ⟨Format.pretty ∘ Level.toFormat⟩

4
library/init/lean/message.lean
View file

@ -54,8 +54,8 @@ instance : HasAppend MessageLog :=
def hasErrors (log : MessageLog) : Bool :=
log.revList.any $ λ m, match m.severity with
| MessageSeverity.error := tt
| _ := ff
| MessageSeverity.error := true
| _ := false
def toList (log : MessageLog) : List Message :=
log.revList.reverse

20
library/init/lean/name.lean
View file

@ -106,24 +106,24 @@ def replacePrefix : Name → Name → Name → Name
mkNumeral (p.replacePrefix queryP newP) s
def quickLtCore : Name → Name → Bool
| anonymous anonymous := ff
| anonymous _ := tt
| (mkNumeral n v) (mkNumeral n' v') := v < v' || (v = v' && n.quickLtCore n')
| (mkNumeral _ _) (mkString _ _) := tt
| (mkString n s) (mkString n' s') := s < s' || (s = s' && n.quickLtCore n')
| _ _ := ff
| anonymous anonymous := false
| anonymous _ := true
| (mkNumeral n v) (mkNumeral n' v') := v < v' || (v = v' && n.quickLtCore n')
| (mkNumeral _ _) (mkString _ _) := true
| (mkString n s) (mkString n' s') := s < s' || (s = s' && n.quickLtCore n')
| _ _ := false
def quickLt (n₁ n₂ : Name) : Bool :=
if n₁.hash < n₂.hash then tt
else if n₁.hash > n₂.hash then ff
if n₁.hash < n₂.hash then true
else if n₁.hash > n₂.hash then false
else quickLtCore n₁ n₂
/- Alternative HasLt instance. -/
@[inline] protected def hasLtQuick : HasLt Name :=
⟨λ a b, Name.quickLt a b = tt⟩
⟨λ a b, Name.quickLt a b = true⟩
@[inline] instance : decidableRel (@HasLt.lt Name Name.hasLtQuick) :=
inferInstanceAs (decidableRel (λ a b, Name.quickLt a b = tt))
inferInstanceAs (decidableRel (λ a b, Name.quickLt a b = true))
def toStringWithSep (sep : String) : Name → String
| anonymous := "[anonymous]"

8
library/init/lean/parser/combinators.lean
View file

@ -86,11 +86,11 @@ private def sepByAux (p : m Syntax) (sep : Parser) (allowTrailingSep : Bool) : B
| pure (Syntax.list (a::as).reverse),
sepByAux allowTrailingSep (s::a::as) n
def sepBy (p sep : Parser) (allowTrailingSep := tt) : Parser :=
do rem ← remaining, sepByAux p sep allowTrailingSep tt [] (rem+1)
def sepBy (p sep : Parser) (allowTrailingSep := true) : Parser :=
do rem ← remaining, sepByAux p sep allowTrailingSep true [] (rem+1)
def sepBy1 (p sep : Parser) (allowTrailingSep := tt) : Parser :=
do rem ← remaining, sepByAux p sep allowTrailingSep ff [] (rem+1)
def sepBy1 (p sep : Parser) (allowTrailingSep := true) : Parser :=
do rem ← remaining, sepByAux p sep allowTrailingSep false [] (rem+1)
instance sepBy.tokens (p sep : Parser) (a) [Parser.HasTokens p] [Parser.HasTokens sep] :
Parser.HasTokens (sepBy p sep a) :=

10
library/init/lean/parser/module.lean
View file

@ -76,11 +76,11 @@ private def commandWrecAux : Bool → Nat → ModuleParserM (Bool × Syntax)
| recovering 0 := error "unreachable"
| recovering (Nat.succ n) := do
-- terminate at EOF
Nat.succ _ ← remaining | (Prod.mk ff) <$> eoi.Parser,
Nat.succ _ ← remaining | (Prod.mk false) <$> eoi.Parser,
(recovering, c) ← catch (do {
cfg ← read,
c ← monadLift $ command.Parser.run cfg.commandParsers,
pure (ff, some c)
pure (false, some c)
} <|> do {
-- unknown command: try to skip token, or else single character
when (¬ recovering) $ do {
@ -88,11 +88,11 @@ private def commandWrecAux : Bool → Nat → ModuleParserM (Bool × Syntax)
logMessage {expected := Dlist.singleton "command", it := it, custom := some ()}
},
try (monadLift token *> pure ()) <|> (any *> pure ()),
pure (tt, none)
pure (true, none)
}) $ λ msg, do {
-- error inside command: log error, return partial Syntax tree
logMessage msg,
pure (tt, some msg.custom.get)
pure (true, some msg.custom.get)
},
/- NOTE: We need to make very sure that these recursive calls are happening in tail positions.
Otherwise, resuming the coroutine is linear in the number of previous commands. -/
@ -120,7 +120,7 @@ match r with
| Except.error msg := (msg.custom.get, Except.error $ messageOfParsecMessage cfg msg)
def parseHeader (cfg : ModuleParserConfig) :=
let snap := {ModuleParserSnapshot . recovering := ff, it := cfg.input.mkIterator} in
let snap := {ModuleParserSnapshot . recovering := false, it := cfg.input.mkIterator} in
resumeModuleParser cfg snap (λ stx, (stx, snap)) $ do
-- `token` assumes that there is no leading whitespace
monadLift whitespace,

2
library/init/lean/parser/notation.lean
View file

@ -68,7 +68,7 @@ def symbolQuote.Parser : termParser :=
node! symbolQuote [
leftQuote: rawStr "`",
symbol: quotedSymbol.Parser,
rightQuote: rawStr "`" tt, -- consume trailing ws
rightQuote: rawStr "`" true, -- consume trailing ws
prec: precedence.Parser?]
def unquotedSymbol.Parser : termParser :=

40
library/init/lean/parser/parsec.lean
View file

@ -94,7 +94,7 @@ def eps : ParsecT μ m Unit :=
ParsecT.pure ()
protected def failure : ParsecT μ m α :=
λ it, pure (error { unexpected := "failure", it := it, custom := none } ff)
λ it, pure (error { unexpected := "failure", it := it, custom := none } false)
def merge (msg₁ msg₂ : Message μ) : Message μ :=
{ expected := msg₁.expected ++ msg₂.expected, ..msg₁ }
@ -102,9 +102,9 @@ def merge (msg₁ msg₂ : Message μ) : Message μ :=
@[inlineIfReduce] def bindMkRes (ex₁ : Option (Dlist String)) (r : Result μ β) : Result μ β :=
match ex₁, r with
| none, ok b it _ := ok b it none
| none, error msg _ := error msg tt
| none, error msg _ := error msg true
| some ex₁, ok b it (some ex₂) := ok b it (some $ ex₁ ++ ex₂)
| some ex₁, error msg₂ ff := error { expected := ex₁ ++ msg₂.expected, .. msg₂ } ff
| some ex₁, error msg₂ false := error { expected := ex₁ ++ msg₂.expected, .. msg₂ } false
| some ex₁, other := other
/--
@ -137,10 +137,10 @@ def Monad' : Monad (ParsecT μ m) :=
{ bind := λ _ _, ParsecT.bind', pure := λ _, ParsecT.pure }
instance : MonadFail Parsec' :=
{ fail := λ _ s it, error { unexpected := s, it := it, custom := () } ff }
{ fail := λ _ s it, error { unexpected := s, it := it, custom := () } false }
instance : MonadExcept (Message μ) (ParsecT μ m) :=
{ throw := λ _ msg it, pure (error msg ff),
{ throw := λ _ msg it, pure (error msg false),
catch := λ _ p c it, do
r ← p it,
match r with
@ -160,7 +160,7 @@ def expect (msg : Message μ) (exp : String) : Message μ :=
@[inlineIfReduce] def labelsMkRes (r : Result μ α) (lbls : Dlist String) : Result μ α :=
match r with
| ok a it (some _) := ok a it (some lbls)
| error msg ff := error {expected := lbls, ..msg} ff
| error msg false := error {expected := lbls, ..msg} false
| other := other
@[inline] def labels (p : ParsecT μ m α) (lbls : Dlist String) : ParsecT μ m α :=
@ -170,7 +170,7 @@ match r with
@[inlineIfReduce] def tryMkRes (r : Result μ α) : Result μ α :=
match r with
| error msg _ := error msg ff
| error msg _ := error msg false
| other := other
/--
@ -198,7 +198,7 @@ Without the `try` Combinator we will not be able to backtrack on the `let` keywo
@[inlineIfReduce] def orelseMkRes (msg₁ : Message μ) (r : Result μ α) : Result μ α :=
match r with
| ok a it' (some ex₂) := ok a it' (some $ msg₁.expected ++ ex₂)
| error msg₂ ff := error (merge msg₁ msg₂) ff
| error msg₂ false := error (merge msg₁ msg₂) false
| other := other
/--
@ -217,7 +217,7 @@ match r with
λ it, do
r ← p it,
match r with
| error msg₁ ff := do { r ← q it, pure $ orelseMkRes msg₁ r }
| error msg₁ false := do { r ← q it, pure $ orelseMkRes msg₁ r }
| other := pure other
instance : Alternative (ParsecT μ m) :=
@ -261,7 +261,7 @@ variables {m : Type → Type} [Monad m] [MonadParsec μ m] {α β : Type}
def error {α : Type} (unexpected : String) (expected : Dlist String := Dlist.Empty)
(it : Option Iterator := none) (custom : Option μ := none) : m α :=
lift $ λ it', Result.error { unexpected := unexpected, expected := expected, it := it.getOrElse it', custom := custom } ff
lift $ λ it', Result.error { unexpected := unexpected, expected := expected, it := it.getOrElse it', custom := custom } false
@[inline] def leftOver : m Iterator :=
lift $ λ it, Result.mkEps it it
@ -315,7 +315,7 @@ do it ← leftOver,
else pure ()
def eoiError (it : Iterator) : Result μ α :=
Result.error { it := it, unexpected := "end of input", custom := default _ } ff
Result.error { it := it, unexpected := "end of input", custom := default _ } false
def curr : m Char :=
String.Iterator.curr <$> leftOver
@ -368,7 +368,7 @@ def strCore (s : String) (ex : Dlist String) : m String :=
if s.isEmpty then pure ""
else lift $ λ it, match strAux s.length s.mkIterator it with
| some it' := Result.ok s it' none
| none := Result.error { it := it, expected := ex, custom := none } ff
| none := Result.error { it := it, expected := ex, custom := none } false
@[inline] def str (s : String) : m String :=
strCore s (Dlist.singleton (repr s))
@ -398,9 +398,9 @@ private def takeWhileAux (p : Char → Bool) : Nat → String → Iterator → R
else mkStringResult r it
/--
Consume input as long as the predicate returns `tt`, and return the consumed input.
Consume input as long as the predicate returns `true`, and return the consumed input.
This Parser does not fail. It will return an Empty String if the predicate
returns `ff` on the current character. -/
returns `false` on the current character. -/
@[specialize] def takeWhile (p : Char → Bool) : m String :=
lift $ λ it, takeWhileAux p it.remaining "" it
@ -408,14 +408,14 @@ lift $ λ it, takeWhileAux p it.remaining "" it
lift $ λ it, takeWhileAux p it.remaining ini it
/--
Consume input as long as the predicate returns `tt`, and return the consumed input.
Consume input as long as the predicate returns `true`, and return the consumed input.
This Parser requires the predicate to succeed on at least once. -/
@[specialize] def takeWhile1 (p : Char → Bool) : m String :=
do c ← satisfy p,
takeWhileCont p (toString c)
/--
Consume input as long as the predicate returns `ff` (i.e. until it returns `tt`), and return the consumed input.
Consume input as long as the predicate returns `false` (i.e. until it returns `true`), and return the consumed input.
This Parser does not fail. -/
@[inline] def takeUntil (p : Char → Bool) : m String :=
takeWhile (λ c, !p c)
@ -432,12 +432,12 @@ else Result.mkEps () it
| (n+1) consumed it :=
if !it.hasNext then mkConsumedResult consumed it
else let c := it.curr in
if p c then takeWhileAux' n tt it.next
if p c then takeWhileAux' n true it.next
else mkConsumedResult consumed it
/-- Similar to `takeWhile` but it does not return the consumed input. -/
@[specialize] def takeWhile' (p : Char → Bool) : m Unit :=
lift $ λ it, takeWhileAux' p it.remaining ff it
lift $ λ it, takeWhileAux' p it.remaining false it
/-- Similar to `takeWhile1` but it does not return the consumed input. -/
@[specialize] def takeWhile1' (p : Char → Bool) : m Unit :=
@ -469,7 +469,7 @@ String.Iterator.offset <$> leftOver
/-- `notFollowedBy p` succeeds when Parser `p` fails -/
@[inline] def notFollowedBy [MonadExcept (Message μ) m] (p : m α) (msg : String := "input") : m Unit :=
do it ← leftOver,
b ← lookahead $ catch (p *> pure ff) (λ _, pure tt),
b ← lookahead $ catch (p *> pure false) (λ _, pure true),
if b then pure () else error msg Dlist.Empty it
def eoi : m Unit :=
@ -554,7 +554,7 @@ do it ← leftOver,
| _ := Result.ok [a] it none)
(λ msg, pure $ match r with
| Result.error msg' _ := if msg'.it.offset > msg.it.offset then r
else if msg.it.offset > msg'.it.offset then Result.error msg tt
else if msg.it.offset > msg'.it.offset then Result.error msg true
else Result.error (merge msg msg') (msg.it.offset > it.offset)
| _ := r))
((error "longestMatch: Empty List" : Parsec _ _) it),

2
library/init/lean/parser/syntax.lean
View file

@ -123,7 +123,7 @@ def kind : Syntax → Option SyntaxNodeKind
def isOfKind (k : SyntaxNodeKind) : Syntax → Bool
| (Syntax.rawNode n) := k.name = n.kind.name
| _ := ff
| _ := false
section
variables {m : Type → Type} [Monad m] (r : Syntax → m (Option Syntax))

8
library/init/lean/parser/term.lean
View file

@ -41,7 +41,7 @@ node! «paren» ["(":maxPrec,
special: nodeChoice! parenSpecial {
/- Do not allow trailing comma. Looks a bit weird and would clash with
adding support for tuple sections (https://downloads.haskell.org/~ghc/8.2.1/docs/html/usersGuide/glasgowExts.html#tuple-sections). -/
tuple: node! tuple [", ", tail: sepBy (Term.Parser 0) (symbol ", ") ff],
tuple: node! tuple [", ", tail: sepBy (Term.Parser 0) (symbol ", ") false],
typed: node! typed [" : ", type: Term.Parser],
}?,
]?,
@ -282,14 +282,14 @@ node! «show» [
def match.Parser : termParser :=
node! «match» [
"match ",
scrutinees: sepBy1 Term.Parser (symbol ", ") ff,
scrutinees: sepBy1 Term.Parser (symbol ", ") false,
type: optType.Parser,
" with ",
optBar: (symbol " | ")?,
equations: sepBy1
node! «matchEquation» [
lhs: sepBy1 Term.Parser (symbol ", ") ff, ":=", rhs: Term.Parser]
(symbol " | ") ff,
lhs: sepBy1 Term.Parser (symbol ", ") false, ":=", rhs: Term.Parser]
(symbol " | ") false,
]
@[derive Parser.HasTokens Parser.HasView]

4
library/init/lean/parser/token.lean
View file

@ -92,7 +92,7 @@ let ss : Substring := ⟨start, stop⟩ in
Syntax.atom ⟨some {leading := ⟨start, start⟩, pos := start.offset, trailing := ⟨stop, stop⟩}, ss.toString⟩
/-- Match an arbitrary Parser and return the consumed String in a `Syntax.atom`. -/
@[inline] def raw {α : Type} (p : m α) (trailingWs := ff) : Parser := do
@[inline] def raw {α : Type} (p : m α) (trailingWs := false) : Parser := do
start ← leftOver,
p,
stop ← leftOver,
@ -108,7 +108,7 @@ instance raw.view {α} (p : m α) (t) : Parser.HasView (Option SyntaxAtom) (raw
/-- Like `raw (str s)`, but default to `s` in views. -/
@[inline, derive HasTokens HasView]
def rawStr (s : String) (trailingWs := ff) : Parser :=
def rawStr (s : String) (trailingWs := false) : Parser :=
raw (str s) trailingWs
instance rawStr.viewDefault (s) (t) : Parser.HasViewDefault (rawStr s t : Parser) (Option SyntaxAtom) (some {val := s}) :=

2
library/init/lean/position.lean
View file

@ -43,7 +43,7 @@ namespace FileMap
private def fromStringAux : Nat → String.Iterator → Nat → List (Nat × Nat)
| 0 it line := []
| (k+1) it line :=
if it.hasNext = ff then []
if it.hasNext = false then []
else match it.curr with
| '\n' := (it.next.offset, line+1) :: fromStringAux k it.next (line+1)
| other := fromStringAux k it.next line

4
library/init/lean/trace.lean
View file

@ -50,7 +50,7 @@ traceCtx cls msg (pure () : m Unit)
instance (m) [Monad m] : MonadTracer (TraceT m) :=
{ traceRoot := λ α pos cls msg ctx, do {
st ← get,
if st.opts.getBool cls = some tt then do {
if st.opts.getBool cls = some true then do {
modify $ λ st, {curPos := pos, curTraces := [], ..st},
a ← ctx.get,
modify $ λ (st : TraceState), {roots := st.roots.insert pos ⟨msg, st.curTraces⟩, ..st},
@ -62,7 +62,7 @@ instance (m) [Monad m] : MonadTracer (TraceT m) :=
-- tracing enabled?
some _ ← pure st.curPos | ctx.get,
-- Trace class enabled?
if st.opts.getBool cls = some tt then do {
if st.opts.getBool cls = some true then do {
put {curTraces := [], ..st},
a ← ctx.get,
modify $ λ (st' : TraceState), {curTraces := st.curTraces ++ [⟨msg, st'.curTraces⟩], ..st'},

2
src/frontends/lean/parser.cpp
View file

@ -172,7 +172,7 @@ void parser::scan() {
}
expr parser::mk_sorry(pos_info const & p, bool synthetic) {
return save_pos(::lean::mk_app(mk_constant(get_sorry_ax_name()), mk_expr_placeholder(), synthetic ? mk_bool_tt() : mk_bool_ff()), p);
return save_pos(::lean::mk_app(mk_constant(get_sorry_ax_name()), mk_expr_placeholder(), synthetic ? mk_bool_true() : mk_bool_false()), p);
}
void parser::updt_options() {

16
src/library/constants.cpp
View file

@ -20,8 +20,8 @@ name const * g_bin_tree_empty = nullptr;
name const * g_bin_tree_leaf = nullptr;
name const * g_bin_tree_node = nullptr;
name const * g_bool = nullptr;
name const * g_bool_ff = nullptr;
name const * g_bool_tt = nullptr;
name const * g_bool_false = nullptr;
name const * g_bool_true = nullptr;
name const * g_combinator_k = nullptr;
name const * g_cast = nullptr;
name const * g_char = nullptr;
@ -304,8 +304,8 @@ void initialize_constants() {
g_bin_tree_leaf = new name{"BinTree", "leaf"};
g_bin_tree_node = new name{"BinTree", "Node"};
g_bool = new name{"Bool"};
g_bool_ff = new name{"Bool", "ff"};
g_bool_tt = new name{"Bool", "tt"};
g_bool_false = new name{"Bool", "false"};
g_bool_true = new name{"Bool", "true"};
g_combinator_k = new name{"Combinator", "K"};
g_cast = new name{"cast"};
g_char = new name{"Char"};
@ -589,8 +589,8 @@ void finalize_constants() {
delete g_bin_tree_leaf;
delete g_bin_tree_node;
delete g_bool;
delete g_bool_ff;
delete g_bool_tt;
delete g_bool_false;
delete g_bool_true;
delete g_combinator_k;
delete g_cast;
delete g_char;
@ -873,8 +873,8 @@ name const & get_bin_tree_empty_name() { return *g_bin_tree_empty; }
name const & get_bin_tree_leaf_name() { return *g_bin_tree_leaf; }
name const & get_bin_tree_node_name() { return *g_bin_tree_node; }
name const & get_bool_name() { return *g_bool; }
name const & get_bool_ff_name() { return *g_bool_ff; }
name const & get_bool_tt_name() { return *g_bool_tt; }
name const & get_bool_false_name() { return *g_bool_false; }
name const & get_bool_true_name() { return *g_bool_true; }
name const & get_combinator_k_name() { return *g_combinator_k; }
name const & get_cast_name() { return *g_cast; }
name const & get_char_name() { return *g_char; }

4
src/library/constants.h
View file

@ -22,8 +22,8 @@ name const & get_bin_tree_empty_name();
name const & get_bin_tree_leaf_name();
name const & get_bin_tree_node_name();
name const & get_bool_name();
name const & get_bool_ff_name();
name const & get_bool_tt_name();
name const & get_bool_false_name();
name const & get_bool_true_name();
name const & get_combinator_k_name();
name const & get_cast_name();
name const & get_char_name();

4
src/library/constants.txt
View file

@ -15,8 +15,8 @@ BinTree.Empty
BinTree.leaf
BinTree.Node
Bool
Bool.ff
Bool.tt
Bool.false
Bool.true
Combinator.K
cast
Char

4
src/library/sorry.cpp
View file

@ -15,7 +15,7 @@ Author: Leonardo de Moura
namespace lean {
expr mk_sorry(abstract_type_context & ctx, expr const & ty, bool synthetic) {
level u = get_level(ctx, ty);
return mk_app(mk_constant(get_sorry_ax_name(), levels(u)), ty, synthetic ? mk_bool_tt() : mk_bool_ff());
return mk_app(mk_constant(get_sorry_ax_name(), levels(u)), ty, synthetic ? mk_bool_true() : mk_bool_false());
}
bool is_sorry(expr const & e) {
@ -26,7 +26,7 @@ bool is_synthetic_sorry(expr const & e) {
if (!is_sorry(e)) return false;
buffer<expr> args;
get_app_args(e, args);
return is_constant(args[1], get_bool_tt_name());
return is_constant(args[1], get_bool_true_name());
}
bool has_synthetic_sorry(expr const & ex) {

18
src/library/util.cpp
View file

@ -964,25 +964,25 @@ expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_k
}
static expr * g_bool = nullptr;
static expr * g_bool_tt = nullptr;
static expr * g_bool_ff = nullptr;
static expr * g_bool_true = nullptr;
static expr * g_bool_false = nullptr;
void initialize_bool() {
g_bool = new expr(mk_constant(get_bool_name()));
g_bool_ff = new expr(mk_constant(get_bool_ff_name()));
g_bool_tt = new expr(mk_constant(get_bool_tt_name()));
g_bool_false = new expr(mk_constant(get_bool_false_name()));
g_bool_true = new expr(mk_constant(get_bool_true_name()));
}
void finalize_bool() {
delete g_bool;
delete g_bool_ff;
delete g_bool_tt;
delete g_bool_false;
delete g_bool_true;
}
expr mk_bool() { return *g_bool; }
expr mk_bool_tt() { return *g_bool_tt; }
expr mk_bool_ff() { return *g_bool_ff; }
expr to_bool_expr(bool b) { return b ? mk_bool_tt() : mk_bool_ff(); }
expr mk_bool_true() { return *g_bool_true; }
expr mk_bool_false() { return *g_bool_false; }
expr to_bool_expr(bool b) { return b ? mk_bool_true() : mk_bool_false(); }
name get_dep_recursor(environment const &, name const & n) {
return name(n, g_rec);

4
src/library/util.h
View file

@ -267,8 +267,8 @@ expr mk_nary_app(expr const & op, buffer<expr> const & nary_args);
expr mk_nary_app(expr const & op, unsigned num_nary_args, expr const * nary_args);
expr mk_bool();
expr mk_bool_tt();
expr mk_bool_ff();
expr mk_bool_true();
expr mk_bool_false();
expr to_bool_expr(bool b);
/* Similar to is_head_beta, but ignores annotations around the function. */