Skip to content

Conversation

@tahina-pro
Copy link
Member

Consider the following 3D data format description:

entrypoint typedef struct _test {
  UINT16 x;
} test;

From this definition, currently, 3D generates F* code that does not typecheck, because entrypoints are not supposed to have a reader, and the way we currently enforce this requirement is to forbid such definitions.

This PR relaxes this requirement to allow those definitions, by casting entrypoint validators with validate_drop to weaken their types.

@tahina-pro tahina-pro merged commit 13688df into master Aug 9, 2024
@tahina-pro tahina-pro deleted the _taramana_3d_no_readable_entrypoint branch August 9, 2024 00:17
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.

2 participants