Skip to content

Some parts of the language are not discussed in the tutorial #4

Open

Description

@peterohanley
  • cn_function
  • pack
  • bitwise functions (operators are not present in the logical language)
  • instantiate ("extract for pure quantifiers")

Activity

  1. bcpierce00 commented on Apr 27, 2024

    @bcpierce00
    Collaborator
  2. dc-mak commented on May 8, 2024

    @dc-mak
    Collaborator

    rems-project/cerberus#230 (comment)

    Just adding here so that it's logged somewhere. You can also have arguments, but the most common case is for constants.

  3. dc-mak commented on May 8, 2024

    @dc-mak
    Collaborator
  4. peterohanley commented on Jun 10, 2024

    @peterohanley
    Author

    It's possible sometimes to write Owned(p) instead of Owned<...>(p) but this is only used in a malloc example, never explicitly mentioned.

  5. samcowger commented on Jul 19, 2024

    @samcowger
    Contributor

    I also don't see any mention of instantiate in the tutorial. It turned out to be necessary for a spec that I wanted to write, which I hope to include in the archive via #49. That example turned out to be a good way for me and @septract to learn about the semantics of instantiate - perhaps it (or something like it) would be a good addition to the tutorial as well.

  6. bcpierce00 commented on Jul 22, 2024

    @bcpierce00
    Collaborator
  7. samcowger commented on Jul 22, 2024

    @samcowger
    Contributor

    Sure, I'll do that.

  8. septract commented on Aug 19, 2024

    @septract
    Collaborator

    We have now disabled pack / unpack, and declared cn_function experimental. So I don't think we need to discuss them in the tutorial.

    This still leaves bitwise functions and instantiate.

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions