mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
3de0460785
This attribute instructs elmiminate_algebraic to keep primitive operations (pattern matching, constructors and projections) on these types. A new option of the transformation, keep_m, instructs it to keep all the monomorphic algebraic datatypes. The rest of the chain is adapted to support monomorphic algebraic types. For now, the only type tagged with this attribute is bool.
7 lines
169 B
Plaintext
7 lines
169 B
Plaintext
theory BuiltIn
|
|
meta "select_inst_default" "local"
|
|
meta "select_lskept_default" "local"
|
|
meta "select_lsinst_default" "local"
|
|
meta "select_kept_default" "all"
|
|
end
|