Change @return! syntax to require ":" after faults. Update all contracts to consistently use ":" before the description.

This commit is contained in:
Christoffer Lerno
2025-03-05 17:11:45 +01:00
parent cf0405930e
commit c0b80eccad
67 changed files with 645 additions and 637 deletions

View File

@@ -11,7 +11,7 @@ struct ByteWriter (OutStream)
<*
@param [&inout] self
@param [&inout] allocator
@require self.bytes.len == 0 "Init may not run on already initialized data"
@require self.bytes.len == 0 : "Init may not run on already initialized data"
@ensure (bool)allocator, self.index == 0
*>
fn ByteWriter* ByteWriter.init(&self, Allocator allocator)
@@ -22,7 +22,7 @@ fn ByteWriter* ByteWriter.init(&self, Allocator allocator)
<*
@param [&inout] self
@require self.bytes.len == 0 "Init may not run on already initialized data"
@require self.bytes.len == 0 : "Init may not run on already initialized data"
@ensure self.index == 0
*>
fn ByteWriter* ByteWriter.tinit(&self)