mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
Split corrected many pattern into two patterns
This commit is contained in:
parent
97556b1b87
commit
eaee313440
@ -506,6 +506,7 @@ builtinsSrc =
|
||||
B "Text.patterns.notCharIn" $ list char --> pat text,
|
||||
-- Pattern.many : Pattern a -> Pattern a
|
||||
B "Pattern.many" $ forall1 "a" (\a -> pat a --> pat a),
|
||||
B "Pattern.many.corrected" $ forall1 "a" (\a -> pat a --> pat a),
|
||||
B "Pattern.replicate" $ forall1 "a" (\a -> nat --> nat --> pat a --> pat a),
|
||||
B "Pattern.capture" $ forall1 "a" (\a -> pat a --> pat a),
|
||||
B "Pattern.captureAs" $ forall1 "a" (\a -> a --> pat a --> pat a),
|
||||
|
@ -3103,7 +3103,9 @@ declareForeigns = do
|
||||
_ -> die "Text.patterns.notCharIn: non-character closure"
|
||||
evaluate . TPat.cpattern . TPat.Char . TPat.Not $ TPat.CharSet cs
|
||||
declareForeign Untracked "Pattern.many" boxDirect . mkForeign $
|
||||
\(TPat.CP p _) -> evaluate . TPat.cpattern $ TPat.Many p
|
||||
\(TPat.CP p _) -> evaluate . TPat.cpattern $ TPat.Many False p
|
||||
declareForeign Untracked "Pattern.many.corrected" boxDirect . mkForeign $
|
||||
\(TPat.CP p _) -> evaluate . TPat.cpattern $ TPat.Many True p
|
||||
declareForeign Untracked "Pattern.capture" boxDirect . mkForeign $
|
||||
\(TPat.CP p _) -> evaluate . TPat.cpattern $ TPat.Capture p
|
||||
declareForeign Untracked "Pattern.captureAs" boxBoxDirect . mkForeign $
|
||||
|
@ -12,7 +12,7 @@ data Pattern
|
||||
| Or Pattern Pattern -- left-biased choice: tries second pattern only if first fails
|
||||
| Capture Pattern -- capture all the text consumed by the inner pattern, discarding its subcaptures
|
||||
| CaptureAs Text Pattern -- capture the given text, discarding its subcaptures, and name the capture
|
||||
| Many Pattern -- zero or more repetitions (at least 1 can be written: Join [p, Many p])
|
||||
| Many Bool Pattern -- zero or more repetitions (at least 1 can be written: Join [p, Many p]); boolean determines whether it works correctly
|
||||
| Replicate Int Int Pattern -- m to n occurrences of a pattern, optional = 0-1
|
||||
| Eof -- succeed if given the empty text, fail otherwise
|
||||
| Literal Text -- succeed if input starts with the given text, advance by that text
|
||||
@ -128,7 +128,7 @@ compile (CaptureAs t p) !err !success = go
|
||||
success' _ rem acc0 _ = success (pushCapture t acc0) rem
|
||||
compiled = compile p err' success'
|
||||
go acc t = compiled acc t acc t
|
||||
compile (Capture (Many (Char Any))) !_ !success = \acc t -> success (pushCapture t acc) Text.empty
|
||||
compile (Capture (Many _ (Char Any))) !_ !success = \acc t -> success (pushCapture t acc) Text.empty
|
||||
compile (Capture c) !err !success = go
|
||||
where
|
||||
err' _ _ acc0 t0 = err acc0 t0
|
||||
@ -152,12 +152,13 @@ compile (Char cp) !err !success = go
|
||||
go acc t = case Text.uncons t of
|
||||
Just (ch, rem) | ok ch -> success acc rem
|
||||
_ -> err acc t
|
||||
compile (Many p) !_ !success = case p of
|
||||
compile (Many correct p) !_ !success = case p of
|
||||
Char Any -> (\acc _ -> success acc Text.empty)
|
||||
Char cp -> walker (charPatternPred cp)
|
||||
p -> go
|
||||
where
|
||||
go = try "Many" (compile p) success success'
|
||||
go | correct = try "Many" (compile p) success success'
|
||||
| otherwise = compile p success success'
|
||||
success' acc rem
|
||||
| Text.size rem == 0 = success acc rem
|
||||
| otherwise = go acc rem
|
||||
|
@ -114,12 +114,12 @@ test =
|
||||
expect' (P.run (P.Char (P.CharSet "0123")) "3ab" == Just ([], "ab"))
|
||||
expect' (P.run (P.Char (P.Not (P.CharSet "0123"))) "a3b" == Just ([], "3b"))
|
||||
expect' (P.run (P.Capture (P.Char (P.Not (P.CharSet "0123")))) "a3b" == Just (["a"], "3b"))
|
||||
expect' (P.run (P.Many (P.Char (P.CharSet "abcd"))) "babbababac123" == Just ([], "123"))
|
||||
expect' (P.run (P.Capture (P.Many (P.Char (P.CharSet "abcd")))) "babbababac123" == Just (["babbababac"], "123"))
|
||||
expect' (P.run (P.Capture (P.Many (P.Char (P.CharClass P.Number)))) "012345abc" == Just (["012345"], "abc"))
|
||||
expect' (P.run (P.Join [P.Capture (P.Many (P.Char (P.CharClass P.Number))), P.Literal ",", P.Capture (P.Many (P.Char P.Any))]) "012345,abc" == Just (["012345", "abc"], ""))
|
||||
expect' (P.run (P.Many True (P.Char (P.CharSet "abcd"))) "babbababac123" == Just ([], "123"))
|
||||
expect' (P.run (P.Capture (P.Many True (P.Char (P.CharSet "abcd")))) "babbababac123" == Just (["babbababac"], "123"))
|
||||
expect' (P.run (P.Capture (P.Many True (P.Char (P.CharClass P.Number)))) "012345abc" == Just (["012345"], "abc"))
|
||||
expect' (P.run (P.Join [P.Capture (P.Many True (P.Char (P.CharClass P.Number))), P.Literal ",", P.Capture (P.Many True (P.Char P.Any))]) "012345,abc" == Just (["012345", "abc"], ""))
|
||||
expect'
|
||||
( P.run (P.Many (P.Join [P.Capture (P.Many (P.Char (P.CharClass P.Number))), P.Many (P.Char (P.CharClass P.Whitespace))])) "01 10 20 1123 292 110 10"
|
||||
( P.run (P.Many True (P.Join [P.Capture (P.Many True (P.Char (P.CharClass P.Number))), P.Many True (P.Char (P.CharClass P.Whitespace))])) "01 10 20 1123 292 110 10"
|
||||
== Just (["01", "10", "20", "1123", "292", "110", "10"], "")
|
||||
)
|
||||
expect' $
|
||||
|
@ -248,6 +248,8 @@
|
||||
builtin-Char.Class.is:termlink
|
||||
builtin-Pattern.captureAs
|
||||
builtin-Pattern.captureAs:termlink
|
||||
builtin-Pattern.many.corrected
|
||||
builtin-Pattern.many.corrected:termlink
|
||||
builtin-Pattern.isMatch
|
||||
builtin-Pattern.isMatch:termlink
|
||||
builtin-IO.fileExists.impl.v3
|
||||
@ -740,6 +742,7 @@
|
||||
(define-builtin-link Universal.compare)
|
||||
(define-builtin-link Universal.murmurHash)
|
||||
(define-builtin-link Pattern.captureAs)
|
||||
(define-builtin-link Pattern.many.corrected)
|
||||
(define-builtin-link Pattern.isMatch)
|
||||
(define-builtin-link Char.Class.is)
|
||||
(define-builtin-link Scope.bytearrayOf)
|
||||
@ -862,6 +865,8 @@
|
||||
(define-unison (builtin-Pattern.captureAs c p)
|
||||
(capture-as c p))
|
||||
|
||||
(define-unison (builtin-Pattern.many.corrected p) (many p))
|
||||
|
||||
(define-unison (builtin-Pattern.isMatch p s)
|
||||
(pattern-match? p s))
|
||||
|
||||
@ -1457,5 +1462,6 @@
|
||||
(declare-builtin-link builtin-Pattern.isMatch)
|
||||
(declare-builtin-link builtin-Scope.bytearrayOf)
|
||||
(declare-builtin-link builtin-Char.Class.is)
|
||||
(declare-builtin-link builtin-Pattern.many.corrected)
|
||||
(declare-builtin-link builtin-unsafe.coerceAbilities)
|
||||
)
|
||||
|
File diff suppressed because it is too large
Load Diff
@ -52,7 +52,7 @@ The `builtins.merge` command adds the known builtins to a `builtin` subnamespace
|
||||
41. Optional (type)
|
||||
42. Optional/ (2 terms)
|
||||
43. Pattern (builtin type)
|
||||
44. Pattern/ (8 terms)
|
||||
44. Pattern/ (9 terms)
|
||||
45. Ref (builtin type)
|
||||
46. Ref/ (2 terms)
|
||||
47. Request (builtin type)
|
||||
|
@ -23,7 +23,7 @@ Technically, the definitions all exist, but they have no names. `builtins.merge`
|
||||
|
||||
.foo> ls
|
||||
|
||||
1. builtin/ (455 terms, 71 types)
|
||||
1. builtin/ (456 terms, 71 types)
|
||||
|
||||
```
|
||||
And for a limited time, you can get even more builtin goodies:
|
||||
@ -35,7 +35,7 @@ And for a limited time, you can get even more builtin goodies:
|
||||
|
||||
.foo> ls
|
||||
|
||||
1. builtin/ (627 terms, 89 types)
|
||||
1. builtin/ (628 terms, 89 types)
|
||||
|
||||
```
|
||||
More typically, you'd start out by pulling `base.
|
||||
|
@ -119,13 +119,13 @@ it's still in the `history` of the parent namespace and can be resurrected at an
|
||||
Note: The most recent namespace hash is immediately below this
|
||||
message.
|
||||
|
||||
⊙ 1. #1qpabd7ooq
|
||||
⊙ 1. #mqis95ft23
|
||||
|
||||
- Deletes:
|
||||
|
||||
feature1.y
|
||||
|
||||
⊙ 2. #jhqb98218p
|
||||
⊙ 2. #5ro9c9692q
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
@ -136,26 +136,26 @@ it's still in the `history` of the parent namespace and can be resurrected at an
|
||||
Original name New name(s)
|
||||
feature1.y master.y
|
||||
|
||||
⊙ 3. #n25372gm2b
|
||||
⊙ 3. #da33td9rni
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
feature1.y
|
||||
|
||||
⊙ 4. #b9s4c5ut48
|
||||
⊙ 4. #ks6rftepdv
|
||||
|
||||
> Moves:
|
||||
|
||||
Original name New name
|
||||
x master.x
|
||||
|
||||
⊙ 5. #9uq9mhup43
|
||||
⊙ 5. #dgcqc7jftr
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
x
|
||||
|
||||
□ 6. #8f47abto6r (start of history)
|
||||
□ 6. #ms344fdodl (start of history)
|
||||
|
||||
```
|
||||
To resurrect an old version of a namespace, you can learn its hash via the `history` command, then use `fork #namespacehash .newname`.
|
||||
|
@ -80,7 +80,7 @@ Should be able to move the term, type, and namespace, including its types, terms
|
||||
1. Bar (Nat)
|
||||
2. Bar (type)
|
||||
3. Bar/ (4 terms, 1 type)
|
||||
4. builtin/ (627 terms, 89 types)
|
||||
4. builtin/ (628 terms, 89 types)
|
||||
|
||||
.> ls Bar
|
||||
|
||||
@ -145,7 +145,7 @@ bonk = 5
|
||||
|
||||
.z> ls
|
||||
|
||||
1. builtin/ (455 terms, 71 types)
|
||||
1. builtin/ (456 terms, 71 types)
|
||||
2. zonk (Nat)
|
||||
|
||||
```
|
||||
@ -188,7 +188,7 @@ bonk.zonk = 5
|
||||
|
||||
.a> ls
|
||||
|
||||
1. builtin/ (455 terms, 71 types)
|
||||
1. builtin/ (456 terms, 71 types)
|
||||
2. zonk/ (1 term)
|
||||
|
||||
.a> view zonk.zonk
|
||||
|
@ -277,7 +277,7 @@ I should be able to move the root into a sub-namespace
|
||||
|
||||
.> ls
|
||||
|
||||
1. root/ (1370 terms, 214 types)
|
||||
1. root/ (1373 terms, 214 types)
|
||||
|
||||
.> history
|
||||
|
||||
@ -286,22 +286,22 @@ I should be able to move the root into a sub-namespace
|
||||
|
||||
|
||||
|
||||
□ 1. #p1ltr60tg9 (start of history)
|
||||
□ 1. #vrn80pdffk (start of history)
|
||||
|
||||
```
|
||||
```ucm
|
||||
.> ls .root.at.path
|
||||
|
||||
1. existing/ (456 terms, 71 types)
|
||||
2. happy/ (458 terms, 72 types)
|
||||
3. history/ (456 terms, 71 types)
|
||||
1. existing/ (457 terms, 71 types)
|
||||
2. happy/ (459 terms, 72 types)
|
||||
3. history/ (457 terms, 71 types)
|
||||
|
||||
.> history .root.at.path
|
||||
|
||||
Note: The most recent namespace hash is immediately below this
|
||||
message.
|
||||
|
||||
⊙ 1. #nndiivp3ng
|
||||
⊙ 1. #g3ri07hi09
|
||||
|
||||
- Deletes:
|
||||
|
||||
@ -312,7 +312,7 @@ I should be able to move the root into a sub-namespace
|
||||
Original name New name
|
||||
existing.a.termInA existing.b.termInA
|
||||
|
||||
⊙ 2. #1he7dqonrt
|
||||
⊙ 2. #ifjg1bj57v
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
@ -324,26 +324,26 @@ I should be able to move the root into a sub-namespace
|
||||
happy.b.termInA existing.a.termInA
|
||||
history.b.termInA existing.a.termInA
|
||||
|
||||
⊙ 3. #fbm4gr3975
|
||||
⊙ 3. #bdn8f7vhg1
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
existing.a.termInA existing.b.termInB
|
||||
|
||||
⊙ 4. #v7j1f8vgni
|
||||
⊙ 4. #5dqmgnr0lt
|
||||
|
||||
> Moves:
|
||||
|
||||
Original name New name
|
||||
history.a.termInA history.b.termInA
|
||||
|
||||
⊙ 5. #ofsvuc0cgu
|
||||
⊙ 5. #vd3d37rn3c
|
||||
|
||||
- Deletes:
|
||||
|
||||
history.b.termInB
|
||||
|
||||
⊙ 6. #s3afu924g2
|
||||
⊙ 6. #gi32sh566a
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
@ -354,13 +354,13 @@ I should be able to move the root into a sub-namespace
|
||||
Original name New name(s)
|
||||
happy.b.termInA history.a.termInA
|
||||
|
||||
⊙ 7. #0bb30gq2b1
|
||||
⊙ 7. #u2bs53f2hl
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
history.a.termInA history.b.termInB
|
||||
|
||||
⊙ 8. #aoclegh6j7
|
||||
⊙ 8. #48hsm89mgl
|
||||
|
||||
> Moves:
|
||||
|
||||
@ -370,7 +370,7 @@ I should be able to move the root into a sub-namespace
|
||||
happy.a.T.T2 happy.b.T.T2
|
||||
happy.a.termInA happy.b.termInA
|
||||
|
||||
⊙ 9. #509sbqajct
|
||||
⊙ 9. #pqd79g3q7l
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
@ -380,7 +380,7 @@ I should be able to move the root into a sub-namespace
|
||||
|
||||
happy.a.T.T
|
||||
|
||||
⊙ 10. #8erj1uau9u
|
||||
⊙ 10. #allrjqq7ga
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
@ -392,7 +392,7 @@ I should be able to move the root into a sub-namespace
|
||||
|
||||
⠇
|
||||
|
||||
⊙ 11. #v4nrp8uols
|
||||
⊙ 11. #ohd0a9rim1
|
||||
|
||||
|
||||
```
|
||||
@ -414,26 +414,26 @@ I should be able to move a sub namespace _over_ the root.
|
||||
.> ls
|
||||
|
||||
1. b/ (3 terms, 1 type)
|
||||
2. builtin/ (455 terms, 71 types)
|
||||
2. builtin/ (456 terms, 71 types)
|
||||
|
||||
.> history
|
||||
|
||||
Note: The most recent namespace hash is immediately below this
|
||||
message.
|
||||
|
||||
⊙ 1. #buu0h3vir1
|
||||
⊙ 1. #lf3m1s2e7i
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
b.T b.T.T1 b.T.T2 b.termInA
|
||||
|
||||
⊙ 2. #rck0cngerk
|
||||
⊙ 2. #b1cg22v7s1
|
||||
|
||||
- Deletes:
|
||||
|
||||
a.T a.T.T1 a.T.T2 a.termInA
|
||||
|
||||
⊙ 3. #k6m6gfsvd6
|
||||
⊙ 3. #r83v608ifd
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
@ -443,13 +443,13 @@ I should be able to move a sub namespace _over_ the root.
|
||||
|
||||
a.T.T
|
||||
|
||||
⊙ 4. #2rvval9cn9
|
||||
⊙ 4. #pmm6a0f6fj
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
a.T a.T.T a.termInA
|
||||
|
||||
□ 5. #schnold03v (start of history)
|
||||
□ 5. #nmcjvlnbk1 (start of history)
|
||||
|
||||
```
|
||||
```ucm
|
||||
|
@ -8,4 +8,5 @@ Some tests of pattern behavior.
|
||||
p1 = join [literal "blue", literal "frog"]
|
||||
|
||||
> Pattern.run (many p1) "bluefrogbluegoat"
|
||||
> Pattern.run (many.corrected p1) "bluefrogbluegoat"
|
||||
```
|
||||
|
@ -4,6 +4,7 @@ Some tests of pattern behavior.
|
||||
p1 = join [literal "blue", literal "frog"]
|
||||
|
||||
> Pattern.run (many p1) "bluefrogbluegoat"
|
||||
> Pattern.run (many.corrected p1) "bluefrogbluegoat"
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -22,6 +23,10 @@ p1 = join [literal "blue", literal "frog"]
|
||||
`>`)... Ctrl+C cancels.
|
||||
|
||||
3 | > Pattern.run (many p1) "bluefrogbluegoat"
|
||||
⧩
|
||||
Some ([], "goat")
|
||||
|
||||
4 | > Pattern.run (many.corrected p1) "bluefrogbluegoat"
|
||||
⧩
|
||||
Some ([], "bluegoat")
|
||||
|
||||
|
@ -63,17 +63,17 @@ y = 2
|
||||
most recent, along with the command that got us there. Try:
|
||||
|
||||
`fork 2 .old`
|
||||
`fork #lbg8tf1sdh .old` to make an old namespace
|
||||
`fork #mq4oqhiuuq .old` to make an old namespace
|
||||
accessible again,
|
||||
|
||||
`reset-root #lbg8tf1sdh` to reset the root namespace and
|
||||
`reset-root #mq4oqhiuuq` to reset the root namespace and
|
||||
its history to that of the
|
||||
specified namespace.
|
||||
|
||||
When Root Hash Action
|
||||
1. now #5gonu2p9gp add
|
||||
2. now #lbg8tf1sdh add
|
||||
3. now #schnold03v builtins.merge
|
||||
1. now #1n5tjujeu7 add
|
||||
2. now #mq4oqhiuuq add
|
||||
3. now #nmcjvlnbk1 builtins.merge
|
||||
4. #sg60bvjo91 history starts here
|
||||
|
||||
Tip: Use `diff.namespace 1 7` to compare namespaces between
|
||||
|
@ -28,13 +28,13 @@ a = 5
|
||||
Note: The most recent namespace hash is immediately below this
|
||||
message.
|
||||
|
||||
⊙ 1. #havp29or07
|
||||
⊙ 1. #0nv4t3770d
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
a
|
||||
|
||||
□ 2. #schnold03v (start of history)
|
||||
□ 2. #nmcjvlnbk1 (start of history)
|
||||
|
||||
.> reset 2
|
||||
|
||||
@ -47,7 +47,7 @@ a = 5
|
||||
|
||||
|
||||
|
||||
□ 1. #schnold03v (start of history)
|
||||
□ 1. #nmcjvlnbk1 (start of history)
|
||||
|
||||
```
|
||||
```unison
|
||||
@ -83,13 +83,13 @@ foo.a = 5
|
||||
Note: The most recent namespace hash is immediately below this
|
||||
message.
|
||||
|
||||
⊙ 1. #i2199da947
|
||||
⊙ 1. #3s91aop8k9
|
||||
|
||||
+ Adds / updates:
|
||||
|
||||
foo.a
|
||||
|
||||
□ 2. #schnold03v (start of history)
|
||||
□ 2. #nmcjvlnbk1 (start of history)
|
||||
|
||||
.> reset 1 foo
|
||||
|
||||
|
@ -13,7 +13,7 @@ Let's look at some examples. We'll start with a namespace with just the builtins
|
||||
|
||||
|
||||
|
||||
□ 1. #iq58l8umv4 (start of history)
|
||||
□ 1. #3pq2vvggng (start of history)
|
||||
|
||||
.> fork builtin builtin2
|
||||
|
||||
@ -42,21 +42,21 @@ Now suppose we `fork` a copy of builtin, then rename `Nat.+` to `frobnicate`, th
|
||||
Note: The most recent namespace hash is immediately below this
|
||||
message.
|
||||
|
||||
⊙ 1. #cb1ngbi7os
|
||||
⊙ 1. #4g884gq7lc
|
||||
|
||||
> Moves:
|
||||
|
||||
Original name New name
|
||||
Nat.frobnicate Nat.+
|
||||
|
||||
⊙ 2. #evasbqug8s
|
||||
⊙ 2. #hnah4l7s0j
|
||||
|
||||
> Moves:
|
||||
|
||||
Original name New name
|
||||
Nat.+ Nat.frobnicate
|
||||
|
||||
□ 3. #iq58l8umv4 (start of history)
|
||||
□ 3. #3pq2vvggng (start of history)
|
||||
|
||||
```
|
||||
If we merge that back into `builtin`, we get that same chain of history:
|
||||
@ -73,21 +73,21 @@ If we merge that back into `builtin`, we get that same chain of history:
|
||||
Note: The most recent namespace hash is immediately below this
|
||||
message.
|
||||
|
||||
⊙ 1. #cb1ngbi7os
|
||||
⊙ 1. #4g884gq7lc
|
||||
|
||||
> Moves:
|
||||
|
||||
Original name New name
|
||||
Nat.frobnicate Nat.+
|
||||
|
||||
⊙ 2. #evasbqug8s
|
||||
⊙ 2. #hnah4l7s0j
|
||||
|
||||
> Moves:
|
||||
|
||||
Original name New name
|
||||
Nat.+ Nat.frobnicate
|
||||
|
||||
□ 3. #iq58l8umv4 (start of history)
|
||||
□ 3. #3pq2vvggng (start of history)
|
||||
|
||||
```
|
||||
Let's try again, but using a `merge.squash` (or just `squash`) instead. The history will be unchanged:
|
||||
@ -108,7 +108,7 @@ Let's try again, but using a `merge.squash` (or just `squash`) instead. The hist
|
||||
|
||||
|
||||
|
||||
□ 1. #iq58l8umv4 (start of history)
|
||||
□ 1. #3pq2vvggng (start of history)
|
||||
|
||||
```
|
||||
The churn that happened in `mybuiltin` namespace ended up back in the same spot, so the squash merge of that namespace with our original namespace had no effect.
|
||||
@ -493,13 +493,13 @@ This checks to see that squashing correctly preserves deletions:
|
||||
Note: The most recent namespace hash is immediately below this
|
||||
message.
|
||||
|
||||
⊙ 1. #272p6p79u5
|
||||
⊙ 1. #jdptkosbfp
|
||||
|
||||
- Deletes:
|
||||
|
||||
Nat.* Nat.+
|
||||
|
||||
□ 2. #iq58l8umv4 (start of history)
|
||||
□ 2. #3pq2vvggng (start of history)
|
||||
|
||||
```
|
||||
Notice that `Nat.+` and `Nat.*` are deleted by the squash, and we see them deleted in one atomic step in the history.
|
||||
|
@ -57,7 +57,7 @@ proj/main> upgrade old new
|
||||
|
||||
proj/main> ls lib
|
||||
|
||||
1. builtin/ (455 terms, 71 types)
|
||||
1. builtin/ (456 terms, 71 types)
|
||||
2. new/ (1 term)
|
||||
|
||||
proj/main> view thingy
|
||||
|
Loading…
Reference in New Issue
Block a user