Lemmas #
Proof that Compiler.Code.compile gives an array with the Compiler.NextOfLt and Capture.Valid property
and has no exceptions
c_compile_spec: main result
theorem
Compiler.Lemmas.compile_nextOf_lt
{states : Array NFA.Unchecked.State}
{captures : Array NFA.Capture}
{groups : Array Nat}
{anchored : Bool}
{expr : Regex.Syntax.Hir}
(h : Code.compile anchored expr (#[], #[], #[]) = EStateM.Result.ok () (states, captures, groups))
:
NextOfLt states
theorem
Compiler.Lemmas.compile_captures_valid
{states : Array NFA.Unchecked.State}
{captures : Array NFA.Capture}
{groups : Array Nat}
{anchored : Bool}
{expr : Regex.Syntax.Hir}
(h : Code.compile anchored expr (#[], #[], #[]) = EStateM.Result.ok () (states, captures, groups))
:
NFA.Capture.Valid captures