mirror of
https://github.com/microsoft/regorus.git
synced 2026-08-05 02:16:11 +00:00
Got cargo build working
This commit is contained in:
@@ -61,11 +61,13 @@ pub assume_specification[ <Number as Clone>::clone ](n: &Number) -> (res: Number
|
||||
res == n,
|
||||
;
|
||||
|
||||
#[cfg(verus_keep_ghost)]
|
||||
pub enum NumberView {
|
||||
Integer(int),
|
||||
Float(f64),
|
||||
}
|
||||
|
||||
#[cfg(verus_keep_ghost)]
|
||||
impl View for Number
|
||||
{
|
||||
type V = NumberView;
|
||||
|
||||
Reference in New Issue
Block a user