fix(library/standard): add missing 'end' of namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
70c0eda9fc
commit
f6ba6da4b5
3 changed files with 4 additions and 0 deletions
|
@ -288,3 +288,5 @@ end
|
||||||
|
|
||||||
-- declare global notation outside the section
|
-- declare global notation outside the section
|
||||||
infixl `++` : 65 := concat
|
infixl `++` : 65 := concat
|
||||||
|
|
||||||
|
end list
|
|
@ -415,3 +415,4 @@ discriminate
|
||||||
-- add_rewrite mul_succ_left mul_succ_right
|
-- add_rewrite mul_succ_left mul_succ_right
|
||||||
-- add_rewrite mul_comm mul_assoc mul_left_comm
|
-- add_rewrite mul_comm mul_assoc mul_left_comm
|
||||||
-- add_rewrite mul_distr_right mul_distr_left
|
-- add_rewrite mul_distr_right mul_distr_left
|
||||||
|
end nat
|
|
@ -137,3 +137,4 @@ calc
|
||||||
... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
|
... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
|
||||||
|
|
||||||
-- TODO: add or_left_comm, and_right_comm, and_left_comm
|
-- TODO: add or_left_comm, and_right_comm, and_left_comm
|
||||||
|
end congr
|
Loading…
Reference in a new issue