unison/unison-src/transcripts/isPropagated-exists.output.md
2021-02-10 22:41:36 -05:00

1.1 KiB

This transcript tests that UCM can always access the definition of IsPropagated/isPropagated, which is used internally.

y depends on x,

x = 3
y = x + 1
.> add

  ⍟ I've added these definitions:
  
    x : Nat
    y : Nat

so the update of x causes a propagated update of y, and UCM links the isPropagated metadata to such resulting terms:

x = 4
.> update

  ⍟ I've updated these names to your new definition:
  
    x : Nat

.> links y

  1. #uqdd5t2fgn : #ffb7g9cull
  
  Tip: Try using `display 1` to display the first result or
       `view 1` to view its source.

.> view 1

  #uqdd5t2fgn : #ffb7g9cull
  #uqdd5t2fgn = #ffb7g9cull#0

Well, it's hard to tell from those hashes, but those are right. We can confirm by running builtins.merge to have UCM add names for them.

.> builtins.merge

  Done.

.> links y

  1. builtin.metadata.isPropagated : IsPropagated
  
  Tip: Try using `display 1` to display the first result or
       `view 1` to view its source.

.> view 1

  builtin.metadata.isPropagated : IsPropagated
  builtin.metadata.isPropagated = IsPropagated