From fbc6bcff924157d705fee819db1d7bb410045032 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Jul 2022 20:53:01 -0700 Subject: [PATCH] chore: remove unnecessary french quotes --- src/Init/Core.lean | 22 +++++++++---------- src/Lean/Attributes.lean | 8 +++---- src/Lean/Data/Lsp/LanguageFeatures.lean | 22 +++++++++---------- src/Lean/Declaration.lean | 28 ++++++++++++------------- src/Lean/Elab/DefView.lean | 20 +++++++++--------- src/Lean/Elab/Do.lean | 8 +++---- src/Lean/ScopedEnvExtension.lean | 4 ++-- 7 files changed, 56 insertions(+), 56 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 9e1451545c..d513fe0ae0 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -97,26 +97,26 @@ export ForIn' (forIn') /-- Auxiliary type used to compile `do` notation. -/ inductive DoResultPRBC (α β σ : Type u) where - | «pure» : α → σ → DoResultPRBC α β σ - | «return» : β → σ → DoResultPRBC α β σ - | «break» : σ → DoResultPRBC α β σ - | «continue» : σ → DoResultPRBC α β σ + | pure : α → σ → DoResultPRBC α β σ + | return : β → σ → DoResultPRBC α β σ + | break : σ → DoResultPRBC α β σ + | continue : σ → DoResultPRBC α β σ /-- Auxiliary type used to compile `do` notation. -/ inductive DoResultPR (α β σ : Type u) where - | «pure» : α → σ → DoResultPR α β σ - | «return» : β → σ → DoResultPR α β σ + | pure : α → σ → DoResultPR α β σ + | return : β → σ → DoResultPR α β σ /-- Auxiliary type used to compile `do` notation. -/ inductive DoResultBC (σ : Type u) where - | «break» : σ → DoResultBC σ - | «continue» : σ → DoResultBC σ + | break : σ → DoResultBC σ + | continue : σ → DoResultBC σ /-- Auxiliary type used to compile `do` notation. -/ inductive DoResultSBC (α σ : Type u) where - | «pureReturn» : α → σ → DoResultSBC α σ - | «break» : σ → DoResultSBC α σ - | «continue» : σ → DoResultSBC α σ + | pureReturn : α → σ → DoResultSBC α σ + | break : σ → DoResultSBC α σ + | continue : σ → DoResultSBC α σ class HasEquiv (α : Sort u) where Equiv : α → α → Sort v diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 30ce345e99..7ac9751aae 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -36,14 +36,14 @@ Note that the attribute handler (`AttributeImpl.add`) is responsible for interpr making sure that these kinds are respected. -/ inductive AttributeKind - | «global» | «local» | «scoped» + | global | «local» | «scoped» deriving BEq, Inhabited instance : ToString AttributeKind where toString - | AttributeKind.global => "global" - | AttributeKind.local => "local" - | AttributeKind.scoped => "scoped" + | .global => "global" + | .local => "local" + | .scoped => "scoped" structure AttributeImpl extends AttributeImplCore where /-- This is run when the attribute is applied to a declaration `decl`. `stx` is the syntax of the attribute including arguments. -/ diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index dde13e1b25..dcbc4aacdd 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -20,10 +20,10 @@ structure CompletionOptions where inductive CompletionItemKind where | text | method | function | constructor | field - | «variable» | «class» | interface | module | property + | variable | class | interface | module | property | unit | value | enum | keyword | snippet | color | file | reference | folder | enumMember - | «constant» | struct | event | operator | typeParameter + | constant | struct | event | operator | typeParameter deriving Inhabited, DecidableEq, Repr instance : ToJson CompletionItemKind where @@ -129,18 +129,18 @@ structure DocumentSymbolParams where inductive SymbolKind where | file | module - | «namespace» + | namespace | package - | «class» + | class | method | property | field | constructor - | «enum» + | enum | interface | function - | «variable» - | «constant» + | variable + | constant | string | number | boolean @@ -228,14 +228,14 @@ structure SymbolInformation where inductive SemanticTokenType where -- Used by Lean | keyword - | «variable» + | variable | property | function /- Other types included by default in the LSP specification. Not used by the Lean core, but useful to users extending the Lean server. -/ - | «namespace» + | namespace | type - | «class» + | class | enum | interface | struct @@ -244,7 +244,7 @@ inductive SemanticTokenType where | enumMember | event | method - | «macro» + | macro | modifier | comment | string diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 84e856d28f..4ac13a136b 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -31,9 +31,9 @@ Remark: the ReducibilityHints are not related to the attributes: reducible/irrel These attributes are used by the Elaborator. The ReducibilityHints are used by the kernel (and Elaborator). Moreover, the ReducibilityHints cannot be changed after a declaration is added to the kernel. -/ inductive ReducibilityHints where - | «opaque» : ReducibilityHints - | «abbrev» : ReducibilityHints - | regular : UInt32 → ReducibilityHints + | opaque : ReducibilityHints + | abbrev : ReducibilityHints + | regular : UInt32 → ReducibilityHints deriving Inhabited @[export lean_mk_reducibility_hints_regular] @@ -49,15 +49,15 @@ def ReducibilityHints.getHeightEx (h : ReducibilityHints) : UInt32 := namespace ReducibilityHints def lt : ReducibilityHints → ReducibilityHints → Bool - | «abbrev», «abbrev» => false - | «abbrev», _ => true - | regular d₁, regular d₂ => d₁ < d₂ - | regular _, «opaque» => true - | _, _ => false + | .abbrev, .abbrev => false + | .abbrev, _ => true + | .regular d₁, .regular d₂ => d₁ < d₂ + | .regular _, .opaque => true + | _, _ => false def isAbbrev : ReducibilityHints → Bool - | «abbrev» => true - | _ => false + | .abbrev => true + | _ => false def isRegular : ReducibilityHints → Bool | regular .. => true @@ -199,7 +199,7 @@ def Declaration.isUnsafeInductiveDeclEx : Declaration → Bool A series of checks are performed by the kernel to check whether a `inductiveDecls` is valid or not. -/ structure InductiveVal extends ConstantVal where - /-- Number of parameters. A parameter is an argument to the defined type that is fixed over constructors. + /-- Number of parameters. A parameter is an argument to the defined type that is fixed over constructors. An example of this is the `α : Type` argument in the vector constructors `nil : Vector α 0` and `cons : α → Vector α n → Vector α (n+1)`. @@ -222,9 +222,9 @@ structure InductiveVal extends ConstantVal where isUnsafe : Bool /-- An inductive type is called reflexive if it has at least one constructor that takes as an argument a function returning the same type we are defining. - Consider the type: + Consider the type: ``` - inductive WideTree where + inductive WideTree where | branch: (Nat -> WideTree) -> WideTree | leaf: WideTree ``` @@ -317,7 +317,7 @@ structure RecursorVal extends ConstantVal where and it is an inductive predicate (ie, it lives in Prop). Examples of inductives with K-like reduction is `Eq`, `Acc`, and `And.intro`. - Non-examples are `exists` (where the constructor has arguments) and + Non-examples are `exists` (where the constructor has arguments) and `Or.intro` (which has multiple constructors). -/ k : Bool diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index ebd6a835cf..a3063d46b4 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -16,22 +16,22 @@ import Lean.Elab.DeclUtil namespace Lean.Elab inductive DefKind where - | «def» | «theorem» | «example» | «opaque» | «abbrev» + | def | theorem | example | opaque | abbrev deriving Inhabited, BEq def DefKind.isTheorem : DefKind → Bool - | «theorem» => true - | _ => false - -def DefKind.isDefOrAbbrevOrOpaque : DefKind → Bool - | «def» => true - | «opaque» => true - | «abbrev» => true + | .theorem => true | _ => false +def DefKind.isDefOrAbbrevOrOpaque : DefKind → Bool + | .def => true + | .opaque => true + | .abbrev => true + | _ => false + def DefKind.isExample : DefKind → Bool - | «example» => true - | _ => false + | .example => true + | _ => false structure DefView where kind : DefKind diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index d01783d71d..24178b9c14 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -191,12 +191,12 @@ inductive Code where joinpoint (name : Name) (params : Array (Var × Bool)) (body : Code) (k : Code) | seq (action : Syntax) (k : Code) | action (action : Syntax) - | «break» (ref : Syntax) - | «continue» (ref : Syntax) - | «return» (ref : Syntax) (val : Syntax) + | break (ref : Syntax) + | continue (ref : Syntax) + | return (ref : Syntax) (val : Syntax) | /-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/ ite (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code) - | «match» (ref : Syntax) (gen : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt Code)) + | match (ref : Syntax) (gen : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt Code)) | jmp (ref : Syntax) (jpName : Name) (args : Array Syntax) deriving Inhabited diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean index 0b8c7740a3..f6e7cde484 100644 --- a/src/Lean/ScopedEnvExtension.lean +++ b/src/Lean/ScopedEnvExtension.lean @@ -12,8 +12,8 @@ namespace Lean namespace ScopedEnvExtension inductive Entry (α : Type) where - | global : α → Entry α - | «scoped» : Name → α → Entry α + | global : α → Entry α + | scoped : Name → α → Entry α structure State (σ : Type) where state : σ