diff --git a/rr_frontend/radium/src/coq/command.rs b/rr_frontend/radium/src/coq/command.rs
index e5fd4e39ec218c86522befa2a010fdfe1dee2d39..98e52c84281e746acc922c857a8b6de500035101 100644
--- a/rr_frontend/radium/src/coq/command.rs
+++ b/rr_frontend/radium/src/coq/command.rs
@@ -16,7 +16,7 @@ use indent_write::fmt::IndentWriter;
use indent_write::indentable::Indentable;
use crate::coq::{
- binder, eval, inductive, module, section, syntax, term, typeclasses, Attribute, Document, ProofDocument,
+ binder, eval, inductive, module, proof, section, syntax, term, Attribute, Document, ProofDocument,
Sentence,
};
use crate::BASE_INDENT;
@@ -113,67 +113,43 @@ pub enum Command {
/// The [`Inductive`] command.
///
/// [`Inductive`]: https://coq.inria.fr/doc/v8.20/refman/language/core/inductive.html#inductive-types
- #[display("{}.", _0)]
+ #[display("{}", _0)]
Inductive(inductive::Inductive),
/// The [`Instance`] command.
///
/// [`Instance`]: https://coq.inria.fr/doc/v8.20/refman/addendum/type-classes.html#coq:cmd.Instance
- #[display("{}.", _0)]
- Instance(typeclasses::Instance),
-
- /// The [`Proof`] command.
- ///
- /// [`Proof`]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Proof
- #[display("Proof.\n{}\n", _0.to_string().indented(BASE_INDENT))]
- Proof(ProofDocument),
-
- /// The [`Proof using`] command.
- ///
- /// [`Proof using`]: https://rocq-prover.org/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Proof-using
- #[display("Proof using {}.\n{}\n", _0.0, _0.1.to_string().indented(BASE_INDENT))]
- ProofUsing((String, ProofDocument)),
-
- /// The [`Defined`] command.
- ///
- /// [`Defined`]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Defined
- #[display("Defined.")]
- Defined,
+ #[display("{}", _0)]
+ Instance(Instance),
/// The [`Open Scope`] command.
///
/// [`Open Scope`]: https://coq.inria.fr/doc/v8.20/refman/user-extensions/syntax-extensions.html#coq:cmd.Open-Scope
- #[display("{}.", _0)]
+ #[display("{}", _0)]
OpenScope(syntax::OpenScope),
- /// The [`Qed`] command.
- ///
- /// [`Qed`]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Qed
- #[display("Qed.")]
- Qed,
-
/// The [`Record`] command.
///
/// [`Record`]: https://coq.inria.fr/doc/v8.20/refman/language/core/records.html#coq:cmd.Record
- #[display("{}.", _0)]
+ #[display("{}", _0)]
Record(term::Record),
/// The [`Context`] command.
///
/// [`Command`]: https://coq.inria.fr/doc/v8.20/refman/language/core/sections.html#coq:cmd.Context
- #[display("{}.", _0)]
+ #[display("{}", _0)]
Context(Context),
/// The [`Definition`] command.
///
/// [`Definition`]: https://coq.inria.fr/doc/v8.20/refman/language/core/definitions.html#coq:cmd.Definition
- #[display("{}.", _0)]
+ #[display("{}", _0)]
Definition(Definition),
/// The [`Lemma`] command.
///
/// [`Lemma`]: https://coq.inria.fr/doc/v8.20/refman/language/core/definitions.html#coq:cmd.Lemma
- #[display("{}.", _0)]
+ #[display("{}", _0)]
Lemma(Lemma),
/// The [`Section`] command.
@@ -233,7 +209,7 @@ impl Context {
impl Display for Context {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- if self.items.0.is_empty() { Ok(()) } else { write!(f, "Context {}", self.items) }
+ if self.items.0.is_empty() { Ok(()) } else { write!(f, "Context {}.", self.items) }
}
}
@@ -243,37 +219,61 @@ pub struct Definition {
pub name: String,
pub params: binder::BinderList,
pub ty: Option<term::Type>,
- pub body: Option<term::Gallina>,
+ pub body: DefinitionBody,
}
impl Display for Definition {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- let mut f2 = IndentWriter::new_skip_initial(BASE_INDENT, &mut *f);
-
if let Some(ty) = &self.ty {
- write!(f2, "Definition {} {} : {ty}", self.name, self.params)?;
+ write!(f, "Definition {} {} : {ty}", self.name, self.params)?;
} else {
- write!(f2, "Definition {} {}", self.name, self.params)?;
+ write!(f, "Definition {} {}", self.name, self.params)?;
}
- if let Some(body) = &self.body {
- write!(f2, " := {}", body)?;
+ match &self.body {
+ DefinitionBody::Term(term) => {
+ writeln!(f, " :=")?;
+ write!(f, "{}.", term.indented(BASE_INDENT))?;
+ },
+
+ DefinitionBody::Proof(proof) => {
+ writeln!(f, ".")?;
+ write!(f, "{}", proof)?;
+ },
}
Ok(())
}
}
+#[derive(Clone, Debug, Eq, PartialEq, Display)]
+pub enum DefinitionBody {
+ #[display("{}", _0)]
+ Term(term::Gallina),
+
+ #[display("{}", _0)]
+ Proof(proof::Proof),
+}
+
/// A Rocq lemma declaration.
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct Lemma {
pub name: String,
pub params: binder::BinderList,
pub ty: term::Type,
+ pub body: proof::Proof,
}
impl Display for Lemma {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- write!(f, "Lemma {} {} : {}\n", self.name, self.params, self.ty)
+ writeln!(f, "Lemma {} {} : {}.", self.name, self.params, self.ty)?;
+ write!(f, "{}", self.body)
}
}
+
+/// The [`Instance`] command.
+///
+/// [`Instance`]: https://coq.inria.fr/doc/v8.20/refman/addendum/type-classes.html#coq:cmd.Instance
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("Instance: {}.\n{}", _0, _1)]
+pub struct Instance(pub term::Type, pub proof::Proof);
diff --git a/rr_frontend/radium/src/coq/inductive.rs b/rr_frontend/radium/src/coq/inductive.rs
index 556e1c059433ddb594c49531877ece4d61c92561..22a3cb6dc4a3012c1ce98f58cebcc213b461ede3 100644
--- a/rr_frontend/radium/src/coq/inductive.rs
+++ b/rr_frontend/radium/src/coq/inductive.rs
@@ -18,7 +18,7 @@ use crate::{display_list, BASE_INDENT};
///
/// [`Inductive`]: https://coq.inria.fr/doc/v8.20/refman/language/core/inductive.html#inductive-types
#[derive(Clone, Eq, PartialEq, Debug, Display, Constructor)]
-#[display("Inductive {} {} :=\n{}\n",
+#[display("Inductive {} {} :=\n{}.\n",
name,
parameters,
display_list!(variants, "\n| ").indented(BASE_INDENT)
diff --git a/rr_frontend/radium/src/coq/ltac.rs b/rr_frontend/radium/src/coq/ltac.rs
index 64659dcd33e2431ac2f788d342a9de191df3604a..b1a50a11657acea274eb01494033d1effedfb99b 100644
--- a/rr_frontend/radium/src/coq/ltac.rs
+++ b/rr_frontend/radium/src/coq/ltac.rs
@@ -26,7 +26,7 @@ pub enum LTac {
/// [`Exact`] tactic
///
- /// [`Exact`]: https://rocq-prover.org/doc/V8.20.1/refman/proof-engine/tactics.html#coq:tacn.exact
+ /// [`Exact`]: https://rocq-prover.org/doc/v8.20/refman/proof-engine/tactics.html#coq:tacn.exact
#[display("exact {}.", _0)]
Exact(term::Gallina),
diff --git a/rr_frontend/radium/src/coq/mod.rs b/rr_frontend/radium/src/coq/mod.rs
index d4d5e7142bbe812a441a839a3b7592d6bf57f8df..9940daf16c85dcdeb7d73e5c330c5972f36f0607 100644
--- a/rr_frontend/radium/src/coq/mod.rs
+++ b/rr_frontend/radium/src/coq/mod.rs
@@ -326,10 +326,10 @@ pub mod eval;
pub mod inductive;
pub mod ltac;
pub mod module;
+pub mod proof;
pub mod section;
pub mod syntax;
pub mod term;
-pub mod typeclasses;
use derive_more::{Deref, DerefMut, Display, From};
use from_variants::FromVariants;
@@ -371,7 +371,7 @@ pub enum Sentence {
/// A [proof document], composed of tactics.
///
-/// [proof document]: https://coq.inria.fr/doc/V8.20/refman/proof-engine/ltac.html#ltac
+/// [proof document]: https://coq.inria.fr/doc/v8.20/refman/proof-engine/ltac.html#ltac
#[derive(Clone, Eq, PartialEq, Debug, Display, Default, Deref, DerefMut)]
#[display("{}\n", display_list!(_0, "\n"))]
pub struct ProofDocument(pub Vec<Vernac>);
@@ -389,7 +389,7 @@ impl ProofDocument {
/// [Vernacular] language, or a comment.
///
-/// [Vernacular]: https://coq.inria.fr/doc/V8.20/refman/proof-engine/ltac.html#grammar-token-ltac_expr
+/// [Vernacular]: https://coq.inria.fr/doc/v8.20/refman/proof-engine/ltac.html#grammar-token-ltac_expr
#[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
pub enum Vernac {
#[display("{}", _0)]
diff --git a/rr_frontend/radium/src/coq/proof.rs b/rr_frontend/radium/src/coq/proof.rs
new file mode 100644
index 0000000000000000000000000000000000000000..24ac9bd8e0d9bb3d4fef76d59d0286ce8c2285c0
--- /dev/null
+++ b/rr_frontend/radium/src/coq/proof.rs
@@ -0,0 +1,65 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// If a copy of the BSD-3-clause license was not distributed with this
+// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
+
+//! The [proof mode].
+//!
+//! [proof mode]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#proof-mode
+
+use std::fmt;
+
+use derive_more::Display;
+use indent_write::fmt::IndentWriter;
+use indent_write::indentable::Indentable;
+
+use crate::{coq, BASE_INDENT};
+
+/// The [`Proof`], or [`Proof using`] command.
+///
+/// [`Proof`]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Proof
+/// [`Proof using`]: https://rocq-prover.org/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Proof-using
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Proof {
+ pub using: Option<String>,
+ pub proof: coq::ProofDocument,
+ pub terminator: Terminator,
+}
+
+impl Display for Proof {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ if let Some(using) = &self.using {
+ writeln!(f, "Proof using {}.", using)?;
+ } else {
+ writeln!(f, "Proof.")?;
+ }
+
+ write!(f, "{}", (&self.proof).indented(BASE_INDENT))?;
+ writeln!(f, "{}.", self.terminator)
+ }
+}
+
+/// A proof terminator, [exiting the proof state].
+///
+/// [exiting the proof state]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#entering-and-exiting-proof-mode
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+pub enum Terminator {
+ /// The [`Admitted`] command.
+ ///
+ /// [`Admitted`]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Admitted
+ #[display("Admitted")]
+ Admitted,
+
+ /// The [`Defined`] command.
+ ///
+ /// [`Defined`]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Defined
+ #[display("Defined")]
+ Defined,
+
+ /// The [`Qed`] command.
+ ///
+ /// [`Qed`]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Qed
+ #[display("Qed")]
+ Qed,
+}
diff --git a/rr_frontend/radium/src/coq/syntax.rs b/rr_frontend/radium/src/coq/syntax.rs
index 8b7280ef2ed4707ddac98951cc0df867053610d8..c010203bc48458f23c40480b7dc84493012d664e 100644
--- a/rr_frontend/radium/src/coq/syntax.rs
+++ b/rr_frontend/radium/src/coq/syntax.rs
@@ -15,7 +15,7 @@ use derive_more::{Deref, DerefMut, Display, From};
/// [`Open Scope`]: https://coq.inria.fr/doc/v8.20/refman/user-extensions/syntax-extensions.html#coq:cmd.Open-Scope
#[derive(Clone, Eq, PartialEq, Debug, Display, Default, Deref, DerefMut, From)]
#[from(forward)]
-#[display("Open Scope {}", _0)]
+#[display("Open Scope {}.", _0)]
pub struct OpenScope(pub String);
impl OpenScope {
diff --git a/rr_frontend/radium/src/coq/typeclasses.rs b/rr_frontend/radium/src/coq/typeclasses.rs
deleted file mode 100644
index 9c35dcd442bd9d5b349daa0cb1cbd61e0c5d64c7..0000000000000000000000000000000000000000
--- a/rr_frontend/radium/src/coq/typeclasses.rs
+++ /dev/null
@@ -1,20 +0,0 @@
-// © 2023, The RefinedRust Developers and Contributors
-//
-// This Source Code Form is subject to the terms of the BSD-3-clause License.
-// If a copy of the BSD-3-clause license was not distributed with this
-// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
-
-//! The [typeclasses] section.
-//!
-//! [typeclasses]: https://coq.inria.fr/doc/v8.20/refman/addendum/type-classes.html
-
-use derive_more::Display;
-
-use crate::coq::term;
-
-/// The [`Instance`] command.
-///
-/// [`Instance`]: https://coq.inria.fr/doc/v8.20/refman/addendum/type-classes.html#coq:cmd.Instance
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("Instance: {}", _0)]
-pub struct Instance(pub term::Type);
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index b5a4cd9ee58b291b4909042397bc72869b0fc307..9d23daaea439e66f508bb8819b18f605fbdecf81 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -17,6 +17,8 @@ use indent_write::fmt::IndentWriter;
use itertools::Itertools;
use log::{info, trace, warn};
+use crate::coq::command::{Definition, DefinitionBody};
+use crate::coq::proof::Proof;
use crate::{coq, display_list, push_str_list, term, write_list, BASE_INDENT};
#[derive(Clone, Debug)]
@@ -1419,50 +1421,52 @@ impl<'def> AbstractVariant<'def> {
ty: Some(ty_params.get_spec_all_type_term(
Box::new(term::RefinedRustType::Ttype(Box::new(self.rfn_type()))).into(),
)),
- body: None,
+ body: coq::command::DefinitionBody::Proof(coq::proof::Proof {
+ using: Some(context_names.join("{}")).filter(|s| !s.is_empty()),
+ proof: {
+ let mut proof_document = coq::ProofDocument::default();
+
+ proof_document.push(coq::Vernac::LTac(coq::ltac::LTac::Exact(coq::term::Gallina::App(
+ Box::new(coq::term::App::new(
+ // TODO: `ty_params` must create a specific Coq object.
+ coq::term::Gallina::Literal(ty_params.to_string()),
+ vec![coq::term::Gallina::Literal(self.get_coq_type_term(sls_app).to_string())],
+ )),
+ ))));
+
+ proof_document
+ },
+ terminator: coq::proof::Terminator::Defined,
+ }),
}));
- {
- let mut proof_document = coq::ProofDocument::default();
-
- proof_document.push(coq::Vernac::LTac(coq::ltac::LTac::Exact(coq::term::Gallina::App(
- Box::new(coq::term::App::new(
- // TODO: `ty_params` must create a specific Coq object.
- coq::term::Gallina::Literal(ty_params.to_string()),
- vec![coq::term::Gallina::Literal(self.get_coq_type_term(sls_app).to_string())],
- )),
- ))));
-
- document.push(coq::command::Command::ProofUsing((context_names.join("{}"), proof_document)));
- document.push(coq::command::Command::Defined);
- }
-
// Generate the refinement type definition
+ let rt_params = all_ty_params.get_coq_ty_rt_params();
+ let using = format!("{} {}", rt_params.make_using_terms(), context_names.join(" "));
+
document.push(coq::command::Command::Definition(coq::command::Definition {
name: self.plain_rt_def_name.clone(),
params: coq::binder::BinderList::empty(),
ty: Some(coq::term::Type::Type),
- body: None,
- }));
-
- {
- let mut proof_document = coq::ProofDocument::default();
-
- let rt_params = all_ty_params.get_coq_ty_rt_params();
- let using = format!("{} {}", rt_params.make_using_terms(), context_names.join(" "));
+ body: coq::command::DefinitionBody::Proof(coq::proof::Proof {
+ using: Some(using).filter(|s| !s.is_empty()),
+ proof: {
+ let mut proof_document = coq::ProofDocument::default();
- proof_document.push(coq::ltac::LTac::LetIn(Box::new(coq::ltac::LetIn::new(
- "__a".to_owned(),
- coq::term::Gallina::App(Box::new(coq::term::App::new(
- coq::term::Gallina::Literal("normalized_rt_of_spec_ty".to_owned()),
- vec![coq::term::Gallina::Literal(self.plain_ty_name.clone())],
- ))),
- coq::ltac::LTac::Exact(coq::term::Gallina::Literal("__a".to_owned())),
- ))));
+ proof_document.push(coq::ltac::LTac::LetIn(Box::new(coq::ltac::LetIn::new(
+ "__a".to_owned(),
+ coq::term::Gallina::App(Box::new(coq::term::App::new(
+ coq::term::Gallina::Literal("normalized_rt_of_spec_ty".to_owned()),
+ vec![coq::term::Gallina::Literal(self.plain_ty_name.clone())],
+ ))),
+ coq::ltac::LTac::Exact(coq::term::Gallina::Literal("__a".to_owned())),
+ ))));
- document.push(coq::command::Command::ProofUsing((using, proof_document)));
- document.push(coq::command::Command::Defined);
- }
+ proof_document
+ },
+ terminator: coq::proof::Terminator::Defined,
+ }),
+ }));
// Make it Typeclasses Transparent
let typeclasses_ty = coq::command::Command::TypeclassesTransparent(self.plain_ty_name.clone());
@@ -2486,20 +2490,20 @@ impl<'def> AbstractEnum<'def> {
document.push(coq::Sentence::Comment(comment));
document.push(coq::command::Command::Inductive(ind.clone()));
+ let mut proof_document = coq::ProofDocument::default();
+ proof_document.push(coq::ltac::LTac::Literal("solve_inhabited".to_owned()));
+
document.push(
- coq::command::CommandAttrs::new(coq::command::Command::Instance(coq::typeclasses::Instance(
+ coq::command::CommandAttrs::new(coq::command::Command::Instance(coq::command::Instance(
coq::term::Type::Literal(format!("Inhabited {}", name)),
+ coq::proof::Proof {
+ using: None,
+ proof: proof_document,
+ terminator: coq::proof::Terminator::Qed,
+ },
)))
.attributes("global"),
);
- {
- let mut proof_document = coq::ProofDocument::default();
-
- proof_document.push(coq::ltac::LTac::Literal("solve_inhabited".to_owned()));
-
- document.push(coq::command::Command::Proof(proof_document));
- document.push(coq::command::Command::Qed);
- }
writeln!(out, "{}", document).unwrap();
}
@@ -3189,7 +3193,7 @@ impl<'def> FunctionSpec<'def, InnerFunctionSpec<'def>> {
name,
params,
ty: Some(coq::term::Type::Literal("spec_with _ _ Prop".to_owned())),
- body: Some(coq::term::Gallina::Literal(quantified_term)),
+ body: coq::command::DefinitionBody::Term(coq::term::Gallina::Literal(quantified_term)),
}
}
}
@@ -3212,7 +3216,7 @@ impl<'def> Display for FunctionSpec<'def, InnerFunctionSpec<'def>> {
name: self.spec_name.clone(),
params,
ty: None,
- body: Some(coq::term::Gallina::Literal(term)),
+ body: coq::command::DefinitionBody::Term(coq::term::Gallina::Literal(term)),
};
doc.push(coq::command::Command::Definition(coq_def));
@@ -4819,7 +4823,7 @@ fn make_trait_instance<'def>(
name: spec_record_name.to_owned(),
params: def_params,
ty: Some(coq::term::Type::Literal(ty_annot)),
- body: Some(coq::term::Gallina::Literal(term_with_specs)),
+ body: coq::command::DefinitionBody::Term(coq::term::Gallina::Literal(term_with_specs)),
}));
Ok(document)
@@ -5000,7 +5004,7 @@ impl<'def> TraitSpecDecl<'def> {
name: spec_incl_name,
params: spec_incl_params,
ty: Some(coq::term::Type::Prop),
- body: Some(body),
+ body: coq::command::DefinitionBody::Term(body),
}
}
@@ -5043,7 +5047,7 @@ impl<'def> TraitSpecDecl<'def> {
name: trait_incl_decl_name.to_owned(),
params,
ty: Some(coq::term::Type::Literal("spec_with _ _ Prop".to_owned())),
- body: Some(coq::term::Gallina::Literal(quantified_term)),
+ body: coq::command::DefinitionBody::Term(coq::term::Gallina::Literal(quantified_term)),
};
let command = coq::command::Command::from(def);
doc.push(command);
@@ -5087,7 +5091,7 @@ impl<'def> Display for TraitSpecDecl<'def> {
// write spec incl relation
let spec_incl_def = self.make_spec_incl_decl();
- write!(f, "{spec_incl_def}.\n")?;
+ write!(f, "{spec_incl_def}\n")?;
// write the individual function specs
for (item_name, item_spec) in &self.default_spec.methods {
@@ -5310,7 +5314,7 @@ impl<'def> TraitImplSpec<'def> {
name: attrs_name.to_owned(),
params: def_rts_params,
ty: Some(attrs_type),
- body: Some(attr_record_term),
+ body: coq::command::DefinitionBody::Term(attr_record_term),
}
}
@@ -5345,7 +5349,7 @@ impl<'def> TraitImplSpec<'def> {
name: spec_name.to_owned(),
params,
ty: None,
- body: Some(coq::term::Gallina::Literal(ty_term)),
+ body: coq::command::DefinitionBody::Term(coq::term::Gallina::Literal(ty_term)),
};
doc.push(coq::command::Command::Definition(lem));
@@ -5368,14 +5372,7 @@ impl<'def> TraitImplSpec<'def> {
let mut ty_term =
format!("{} {}", self.trait_ref.impl_ref.spec_subsumption_statement, params.make_using_terms());
- let lem = coq::command::Lemma {
- name: lemma_name.to_owned(),
- params,
- ty: coq::term::Type::Literal(ty_term),
- };
- doc.push(coq::command::Command::Lemma(lem));
-
- {
+ let proof_doc = {
let mut proof_doc = coq::ProofDocument::default();
let prelude_tac = format!(
@@ -5390,9 +5387,21 @@ impl<'def> TraitImplSpec<'def> {
proof_doc.push(coq::ltac::LTac::Literal("Unshelve".to_owned()));
proof_doc.push(coq::ltac::LTac::Literal("all: sidecond_hammer".to_owned()));
- doc.push(coq::command::Command::Proof(proof_doc));
- doc.push(coq::command::Command::Qed);
- }
+ proof_doc
+ };
+
+ let lem = coq::command::Lemma {
+ name: lemma_name.to_owned(),
+ params,
+ ty: coq::term::Type::Literal(ty_term),
+ body: coq::proof::Proof {
+ using: None,
+ proof: proof_doc,
+ terminator: coq::proof::Terminator::Qed,
+ },
+ };
+
+ doc.push(coq::command::Command::Lemma(lem));
doc
}
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index a1469d66675c44d5b8d19620541f24c36425232e..da779ab9cba860c64d733b7556d3619bdc250fd9 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -541,7 +541,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
writeln!(spec_file, "Section attrs.").unwrap();
writeln!(spec_file, "Context `{{RRGS : !refinedrustGS Σ}}.").unwrap();
for spec in self.trait_impls.values() {
- writeln!(spec_file, "{}.\n", spec.generate_attr_decl()).unwrap();
+ writeln!(spec_file, "{}\n", spec.generate_attr_decl()).unwrap();
}
writeln!(spec_file, "End attrs.\n").unwrap();
}