feat(library): reorganize and declare some notation
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
58e325f0af
commit
89380f088e
4 changed files with 66 additions and 41 deletions
|
|
@ -1,6 +1,15 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.function
|
||||
Author: Leonardo de Moura
|
||||
|
||||
General operations on functions.
|
||||
-/
|
||||
|
||||
import general_notation
|
||||
|
||||
namespace function
|
||||
|
||||
variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
|
||||
|
|
@ -20,7 +29,8 @@ definition combine (f : A → B → C) (op : C → D → E) (g : A → B → D)
|
|||
definition const {A : Type} (B : Type) (a : A) : B → A :=
|
||||
λx, a
|
||||
|
||||
definition dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type} (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
|
||||
definition dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type}
|
||||
(f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
|
||||
λx, f (g x)
|
||||
|
||||
definition flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
|
||||
|
|
@ -29,7 +39,6 @@ definition flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y)
|
|||
definition app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x :=
|
||||
f x
|
||||
|
||||
precedence `∘`:60
|
||||
precedence `∘'`:60
|
||||
precedence `on`:1
|
||||
precedence `$`:1
|
||||
|
|
|
|||
|
|
@ -1,6 +1,11 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: data.prod.decl
|
||||
Author: Leonardo de Moura, Jeremy Avigad
|
||||
-/
|
||||
|
||||
import data.unit.decl logic.eq
|
||||
|
||||
structure prod (A B : Type) :=
|
||||
|
|
@ -10,6 +15,12 @@ definition pair := @prod.mk
|
|||
|
||||
namespace prod
|
||||
notation A × B := prod A B
|
||||
notation A * B := prod A B
|
||||
namespace low_precedence_times
|
||||
reserve infixr `*`:30 -- conflicts with notation for multiplication
|
||||
infixr `*` := prod
|
||||
end low_precedence_times
|
||||
|
||||
notation `pr₁` := pr1
|
||||
notation `pr₂` := pr2
|
||||
|
||||
|
|
|
|||
|
|
@ -1,23 +1,23 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: data.sum
|
||||
Authors: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
The sum type, aka disjoint union.
|
||||
-/
|
||||
|
||||
import logic.prop logic.inhabited logic.decidable
|
||||
open inhabited decidable eq.ops
|
||||
|
||||
-- data.sum
|
||||
-- ========
|
||||
-- The sum type, aka disjoint union.
|
||||
|
||||
inductive sum (A B : Type) : Type :=
|
||||
inl : A → sum A B,
|
||||
inr : B → sum A B
|
||||
|
||||
namespace sum
|
||||
|
||||
notation A ⊎ B := sum A B
|
||||
notation A + B := sum A B
|
||||
|
||||
namespace low_precedence_plus
|
||||
reserve infixr `+`:25 -- conflicts with notation for addition
|
||||
infixr `+` := sum
|
||||
|
|
@ -35,15 +35,16 @@ namespace sum
|
|||
theorem inr_inj : inr A b₁ = inr A b₂ → b₁ = b₂ :=
|
||||
assume H, no_confusion H (λe, e)
|
||||
|
||||
protected definition is_inhabited_left [instance] : inhabited A → inhabited (A ⊎ B) :=
|
||||
protected definition is_inhabited_left [instance] : inhabited A → inhabited (A + B) :=
|
||||
assume H : inhabited A, inhabited.mk (inl B (default A))
|
||||
|
||||
protected definition is_inhabited_right [instance] : inhabited B → inhabited (A ⊎ B) :=
|
||||
protected definition is_inhabited_right [instance] : inhabited B → inhabited (A + B) :=
|
||||
assume H : inhabited B, inhabited.mk (inr A (default B))
|
||||
|
||||
protected definition has_eq_decidable [instance] : decidable_eq A → decidable_eq B → decidable_eq (A ⊎ B) :=
|
||||
protected definition has_eq_decidable [instance] :
|
||||
decidable_eq A → decidable_eq B → decidable_eq (A + B) :=
|
||||
assume (H₁ : decidable_eq A) (H₂ : decidable_eq B),
|
||||
take s₁ s₂ : A ⊎ B,
|
||||
take s₁ s₂ : A + B,
|
||||
rec_on s₁
|
||||
(take a₁, show decidable (inl B a₁ = s₂), from
|
||||
rec_on s₂
|
||||
|
|
|
|||
|
|
@ -1,25 +1,27 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
/-
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
-- general_notation
|
||||
-- ================
|
||||
Module: general_notation
|
||||
Authors: Leonardo de Moura, Jeremy Avigad
|
||||
-/
|
||||
|
||||
-- General operations
|
||||
-- ------------------
|
||||
/- General operations -/
|
||||
|
||||
notation `assume` binders `,` r:(scoped f, f) := r
|
||||
notation `take` binders `,` r:(scoped f, f) := r
|
||||
|
||||
-- Global declarations of right binding strength
|
||||
-- ---------------------------------------------
|
||||
/-
|
||||
Global declarations of right binding strength
|
||||
|
||||
-- If a module reassigns these, it will be incompatible with other modules that adhere to these
|
||||
-- conventions.
|
||||
If a module reassigns these, it will be incompatible with other modules that adhere to these
|
||||
conventions.
|
||||
|
||||
-- When hovering over a symbol, use "C-u C-x =" to see how to input it
|
||||
When hovering over a symbol, use "C-u C-x =" to see how to input it.
|
||||
-/
|
||||
|
||||
/- Logical operations and relations -/
|
||||
|
||||
-- ### Logical operations and relations
|
||||
reserve prefix `¬`:40
|
||||
reserve prefix `~`:40
|
||||
reserve infixr `∧`:35
|
||||
|
|
@ -33,16 +35,17 @@ reserve infix `≠`:50
|
|||
reserve infix `≈`:50
|
||||
reserve infix `∼`:50
|
||||
|
||||
reserve infix `∘`:60 -- input with \comp
|
||||
reserve postfix `⁻¹`:100 --input with \sy or \-1 or \inv
|
||||
reserve infixl `⬝`:75
|
||||
reserve infixr `▸`:75
|
||||
|
||||
-- ### types and type constructors
|
||||
/- types and type constructors -/
|
||||
|
||||
reserve infixl `⊎`:25
|
||||
reserve infixl `×`:30
|
||||
|
||||
-- ### arithmetic operations
|
||||
/- arithmetic operations -/
|
||||
|
||||
reserve infixl `+`:65
|
||||
reserve infixl `-`:65
|
||||
|
|
@ -58,18 +61,19 @@ reserve infix `>=`:50
|
|||
reserve infix `≥`:50
|
||||
reserve infix `>`:50
|
||||
|
||||
-- ### boolean operations
|
||||
/- boolean operations -/
|
||||
|
||||
reserve infixl `&&`:70
|
||||
reserve infixl `||`:65
|
||||
|
||||
-- ### set operations
|
||||
/- set operations -/
|
||||
|
||||
reserve infix `∈`:50
|
||||
reserve infixl `∩`:70
|
||||
reserve infixl `∪`:65
|
||||
|
||||
-- ### other symbols
|
||||
/- other symbols -/
|
||||
|
||||
precedence `|`:55
|
||||
reserve notation | a:55 |
|
||||
reserve infixl `++`:65
|
||||
|
|
|
|||
Loading…
Reference in a new issue