| 98 | /// A declaration of a term with its argument and return types. |
| 99 | #[derive(Clone, PartialEq, Eq, Debug)] |
| 100 | pub struct Decl { |
| 101 | pub term: Ident, |
| 102 | pub arg_tys: Vec<Ident>, |
| 103 | pub ret_ty: Ident, |
| 104 | /// Whether this term's constructor is pure. |
| 105 | pub pure: bool, |
| 106 | /// Whether this term can exist with some multiplicity: an |
| 107 | /// extractor or a constructor that matches multiple times, or |
| 108 | /// produces multiple values. |
| 109 | pub multi: bool, |
| 110 | /// Whether this term's constructor can fail to match. |
| 111 | pub partial: bool, |
| 112 | /// Whether this term is permitted to be recursive. |
| 113 | pub rec: bool, |
| 114 | pub pos: Pos, |
| 115 | } |
| 116 | |
| 117 | /// An expression used to specify term semantics, similar to SMT-LIB syntax. |
| 118 | #[derive(Clone, PartialEq, Eq, Debug)] |