On Design of Move Prover

Owned by Xudong Wang

Last updated: 4月 29, 2022

1 min read

1. Thoughts of MVP Features

1.1 Refering to Generic Parameter types in Spec lang [1]

native name_of<T>();
spec schema name_of {
   forall t: type...
}

1.2 Don’t check generic “struct” constraints in spec scheme [1]

Example:

spec schema FooSchema<T> {
  aborts_if exists<T>(0x123);
}

TODO: Describe it later