Skip to content

Commit 38877b8

Browse files
authored
Uncomment ceiling and floor symbols (#6)
Closes #5
1 parent 97137d8 commit 38877b8

File tree

2 files changed

+8
-8
lines changed

2 files changed

+8
-8
lines changed

docs/agda.js

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -249,13 +249,13 @@
249249
// ["cu", "⌜⌝ ⌈⌉ "],
250250
// ["cl", " ⌞⌟ ⌊⌋"],
251251
// ["cul", "⌜"],
252-
// ["cuL", "⌈"],
252+
["cuL", "⌈"],
253253
// ["cur", "⌝"],
254-
// ["cuR", "⌉"],
254+
["cuR", "⌉"],
255255
// ["cll", "⌞"],
256-
// ["clL", "⌊"],
256+
["clL", "⌊"],
257257
// ["clr", "⌟"],
258-
// ["clR", "⌋"],
258+
["clR", "⌋"],
259259

260260
// Various operators/symbols.
261261
["qed", "∎"],

src/translations.js

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -153,13 +153,13 @@ export const translations = toTable([
153153
// ["cu", "⌜⌝ ⌈⌉ "],
154154
// ["cl", " ⌞⌟ ⌊⌋"],
155155
// ["cul", "⌜"],
156-
// ["cuL", "⌈"],
156+
["cuL", "⌈"],
157157
// ["cur", "⌝"],
158-
// ["cuR", "⌉"],
158+
["cuR", "⌉"],
159159
// ["cll", "⌞"],
160-
// ["clL", "⌊"],
160+
["clL", "⌊"],
161161
// ["clr", "⌟"],
162-
// ["clR", "⌋"],
162+
["clR", "⌋"],
163163

164164
// Various operators/symbols.
165165
["qed", "∎"],

0 commit comments

Comments
 (0)