Skip to content

Conversation

@chenyan-dfinity
Copy link
Contributor

Fix #295

chenyan-dfinity and others added 2 commits January 13, 2022 13:45
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
nomeata added a commit to nomeata/candid that referenced this pull request Feb 10, 2022
@nomeata
Copy link
Contributor

nomeata commented Feb 10, 2022

#316 has early explorations of updating the Coq proof for this, but stuck at various technicalities right now. For example

Lemma coerce_roundtrip:
  forall t1 v1,
  v1 :: t1 ->
  coerce t1 t1 v1 = Some v1.

doesn't work with our “untyped values” in the formalization because :: allows any reference value at any type.

Co-authored-by: Claudio Russo <claudio@dfinity.org>
@nomeata
Copy link
Contributor

nomeata commented Oct 7, 2022

Oh, this hasn't landed yet? Completely forgot… I guess we are waiting for all implementations to catch up?

@crusso
Copy link
Contributor

crusso commented Oct 26, 2022

Oh, this hasn't landed yet? Completely forgot… I guess we are waiting for all implementations to catch up?

@chenyan-dfinity is working on it. Motoko is hopefully ready to go (though I'm worried even I don't understand that implementation any more).

Co-authored-by: Claudio Russo <claudio@dfinity.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
@chenyan-dfinity chenyan-dfinity marked this pull request as ready for review December 4, 2022 22:31
@chenyan-dfinity chenyan-dfinity merged commit 6edd82f into master Dec 4, 2022
@chenyan-dfinity chenyan-dfinity deleted the spec-variant branch December 4, 2022 22:39
@nomeata
Copy link
Contributor

nomeata commented Dec 5, 2022

🥳

I have released haskell-candid 0.4 with the corresponding changes (nomeata/haskell-candid#20).

Maybe someone can help me with dfinity/ic-hs#118?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Extensible variants

3 participants