mark the parser type of set_parser erasable

With that, parser extraction SUCCEEDS!
project-everest · Feb 12, 2025 · 1c2b14f · 1c2b14f
1 parent b857fcd
commit 1c2b14f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/cddl/pulse/CDDL.Pulse.Bundle.ArrayGroup.fst b/src/cddl/pulse/CDDL.Pulse.Bundle.ArrayGroup.fst
@@ -39,7 +39,7 @@ let array_bundle_set_parser
   ([@@@erasable] b: Ghost.erased (array_bundle cbor_array_iterator_match))
   (t: Type0)
   ([@@@erasable] t_eq: squash (t == b.ab_impl_type))
-  (#t': Type)
+  (#[@@@erasable] t': Type)
   (p: t')
   ([@@@erasable] p_eq: squash (t' == impl_zero_copy_array_group cbor_array_iterator_match b.ab_spec.ag_parser b.ab_rel))
 : Tot (array_bundle cbor_array_iterator_match)

diff --git a/src/cddl/pulse/CDDL.Pulse.Bundle.Base.fst b/src/cddl/pulse/CDDL.Pulse.Bundle.Base.fst
@@ -41,7 +41,7 @@ let bundle_set_parser
   ([@@@erasable] b: Ghost.erased (bundle vmatch))
   (t: Type0)
   ([@@@erasable] t_eq: squash (t == b.b_impl_type))
-  (#t': Type)
+  (#[@@@erasable] t': Type)
   (p: t')
   ([@@@erasable] p_eq: squash (t' == impl_zero_copy_parse vmatch b.b_spec.parser b.b_rel))
 : Tot (bundle vmatch)