-
Notifications
You must be signed in to change notification settings - Fork 19
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix(proof-libs): reflect
alloc changes
- Loading branch information
Showing
1 changed file
with
15 additions
and
16 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,28 +1,27 @@ | ||
| module Alloc.Collections.Binary_heap | ||
| open Rust_primitives | ||
|
|
||
| val t_BinaryHeap: Type -> eqtype | ||
| val t_BinaryHeap: Type -> unit -> eqtype | ||
|
|
||
| val impl_9__new: #t:Type -> t_BinaryHeap t | ||
| val impl_9__push: #t:Type -> t_BinaryHeap t -> t -> t_BinaryHeap t | ||
| val impl_10__len: #t:Type -> t_BinaryHeap t -> usize | ||
| val impl_10__iter: #t:Type -> t_BinaryHeap t -> t_Slice t | ||
| val impl_10__new: #t:Type -> t_BinaryHeap t () | ||
| val impl_10__push: #t:Type -> t_BinaryHeap t () -> t -> t_BinaryHeap t () | ||
| val impl_11__len: #t:Type -> t_BinaryHeap t () -> usize | ||
| val impl_11__iter: #t:Type -> t_BinaryHeap t () -> t_Slice t | ||
|
|
||
| open Core.Option | ||
|
|
||
| val impl_10__peek: #t:Type -> t_BinaryHeap t -> t_Option t | ||
| val impl_9__pop: #t:Type -> t_BinaryHeap t -> t_BinaryHeap t & t_Option t | ||
| val impl_11__peek: #t:Type -> t_BinaryHeap t () -> t_Option t | ||
| val impl_10__pop: #t:Type -> t_BinaryHeap t () -> t_BinaryHeap t () & t_Option t | ||
|
|
||
| unfold | ||
| let nonempty h = v (impl_10__len h) > 0 | ||
| let nonempty h = v (impl_11__len h) > 0 | ||
|
|
||
| val lemma_peek_len: #t:Type -> h: t_BinaryHeap t | ||
| -> Lemma (Option_Some? (impl_10__peek h) <==> nonempty h) | ||
| val lemma_peek_len: #t:Type -> h: t_BinaryHeap t () | ||
| -> Lemma (Option_Some? (impl_11__peek h) <==> nonempty h) | ||
|
|
||
| val lemma_pop_len: #t:Type -> h: t_BinaryHeap t | ||
| -> Lemma (Option_Some? (snd (impl_9__pop h)) <==> nonempty h) | ||
|
|
||
| val lemma_peek_pop: #t:Type -> h: t_BinaryHeap t | ||
| -> Lemma (impl_10__peek h == snd (impl_9__pop h)) | ||
| [SMTPat (impl_10__peek h)] | ||
| val lemma_pop_len: #t:Type -> h: t_BinaryHeap t () | ||
| -> Lemma (Option_Some? (snd (impl_10__pop h)) <==> nonempty h) | ||
|
|
||
| val lemma_peek_pop: #t:Type -> h: t_BinaryHeap t () | ||
| -> Lemma (impl_11__peek h == snd (impl_10__pop h)) | ||
| [SMTPat (impl_11__peek h)] |