Skip to content

GitLab

Commit 44e07b78 authored by Michael Sammler's avatar Michael Sammler
Browse files

export bitfield type again

parent 51c5ff95
Pipeline #52550 passed with stage
in 18 minutes and 13 seconds
Hide whitespace changes
Inline Side-by-side
theories/typing/typing.v
View file @ 44e07b78
From refinedc.lang Require Export bitfield.
From refinedc.typing Require Export programs type int intptr function bytes own struct optional singleton fixpoint automation padded exist immovable constrained union array wand globals tyfold atomic_bool locked tagged_ptr.
From refinedc.typing Require Export programs type int intptr function bytes own struct optional singleton fixpoint automation padded exist immovable constrained union array wand globals tyfold atomic_bool locked tagged_ptr bitfield.
Notation "'block{' n }" := (typed_block _ n _ _ _ _) (only printing, format "'block{' n }") : bi_scope.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment