Skip to content
Snippets Groups Projects
Verified Commit 7f81a4da authored by Vincent Lafeychine's avatar Vincent Lafeychine
Browse files

chore(coq::term): Add internal type VariantList

parent dee62ee0
No related branches found
No related tags found
1 merge request!55Refactor `coq` crate
......@@ -359,13 +359,15 @@ impl Variant {
}
#[derive(Clone, Eq, PartialEq, Debug, Display)]
#[display("Inductive {} {} :=\n{}\n.", name, parameters,
display_list!(variants, "\n| ").indented(&make_indent(1))
)]
#[display("{}", display_list!(_0, "\n| "))]
struct VariantList(Vec<Variant>);
#[derive(Clone, Eq, PartialEq, Debug, Display)]
#[display("Inductive {} {} :=\n{}\n.", name, parameters, variants.indented(&make_indent(1)))]
pub struct Inductive {
name: String,
parameters: ParamList,
variants: Vec<Variant>,
variants: VariantList,
}
impl Inductive {
......@@ -373,8 +375,8 @@ impl Inductive {
pub fn new(name: &str, parameters: Vec<Param>, variants: Vec<Variant>) -> Self {
Self {
name: name.to_owned(),
parameters: ParamList::new(parameters),
variants,
parameters: ParamList(parameters),
variants: VariantList(variants),
}
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment