let concl = (term2pres t) in
if conclude.Con.conclude_method = "BU_Conversion" then
make_concl "that is equivalent to" concl
+ else if conclude.Con.conclude_method = "FalseInd" then
+ (* false ind is in charge to add the conclusion *)
+ falseind conclude
else
let conclude_body = conclude_aux conclude in
let ann_concl =
exists conclude
else if (conclude.Con.conclude_method = "AndInd") then
andind conclude
+ else if (conclude.Con.conclude_method = "FalseInd") then
+ falseind conclude
else if (conclude.Con.conclude_method = "Rewrite") then
let justif =
(match (List.nth conclude.Con.conclude_args 6) with
P.Mtext([None,"mathcolor","Red"],"with");
P.Mspace([None,"width","0.1cm"]);term2]))]);
P.Mtr ([],[P.Mtd ([],P.indented justif)])]);
-(* OLD CODE
- let conclusion =
- (match conclude.Con.conclude_conclusion with
- None -> P.Mtext([],"NO Conclusion!!!")
- | Some c -> term2pres c) in
- P.Mtable ([None,"align","baseline 1";None,"equalrows","false";
- None,"columnalign","left"],
- [P.Mtr ([],[P.Mtd ([],P.Mrow([],[
- P.Mtext([None,"mathcolor","Red"],"rewrite");
- P.Mspace([None,"width","0.1cm"]);term1;
- P.Mspace([None,"width","0.1cm"]);
- P.Mtext([None,"mathcolor","Red"],"with");
- P.Mspace([None,"width","0.1cm"]);term2]))]);
- P.Mtr ([],[P.Mtd ([],P.indented justif)]);
- P.Mtr ([],[P.Mtd ([],make_concl "we proved 2" conclusion)])]) *)
else if conclude.Con.conclude_method = "Apply" then
let pres_args =
make_args_for_apply term2pres conclude.Con.conclude_args in
P.Mtext([None,"mathcolor","Red"],"by")::
P.Mspace([None,"width","0.1cm"])::
P.Mo([],"(")::pres_args@[P.Mo([],")")])
-(* OLD CODE
- let by =
- P.Mrow([],
- P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
- P.Mo([],"(")::pres_args@[P.Mo([],")")]) in
- match conclude.Con.conclude_conclusion with
- None -> P.Mrow([],[P.Mtext([],"QUA");by])
- | Some t ->
- let concl = (term2pres t) in
- let ann_concl = make_concl "we proved 3" concl in
- P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
- None,"columnalign","left";
- Some "helm", "xref", conclude.Con.conclude_id],
- [P.Mtr ([],[P.Mtd ([],by)]);
- P.Mtr ([],[P.Mtd ([],ann_concl)])]) *)
else
P.Mtable
([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
([None,"align","baseline 1"; None,"equalrows","false";
None,"columnalign","left"],
args2pres conclude.Con.conclude_args))))])])
-(* OLD CODE
- match conclude.Con.conclude_conclusion with
- None -> body
- | Some t ->
- let concl = (term2pres t) in
- let ann_concl = make_concl "we proved 4" concl in
- P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
- None,"columnalign","left"],
- [P.Mtr ([],[P.Mtd ([],body)]);
- P.Mtr ([],[P.Mtd ([],ann_concl)])]) *)
and args2pres l =
let module P = Mpresentation in
[P.Mtr([],[P.Mtd([],presacontext)])])
| _ -> assert false
+ and falseind conclude =
+ let module P = Mpresentation in
+ let module Con = Content in
+ let proof_conclusion =
+ (match conclude.Con.conclude_conclusion with
+ None -> P.Mtext([],"No conclusion???")
+ | Some t -> term2pres t) in
+ let case_arg =
+ (match conclude.Con.conclude_args with
+ [Con.Aux(n);_;case_arg] -> case_arg
+ | _ -> assert false;
+ (*
+ List.map (ContentPp.parg 0) conclude.Con.conclude_args;
+ assert false *)) in
+ let arg =
+ (match case_arg with
+ Con.Aux n -> assert false
+ | Con.Premise prem ->
+ (match prem.Con.premise_binder with
+ None -> [P.Mtext([],"Contradiction, hence")]
+ | Some n ->
+ [P.Mi([],n);P.smallskip;P.Mtext([],"is contradictory, hence")])
+ | Con.Lemma lemma ->
+ [P.Mi([],lemma.Con.lemma_name);P.smallskip;P.Mtext([],"is contradictory, hence")]
+ | _ -> assert false) in
+ (* let body = proof2pres {proof with Con.proof_context = tl} in *)
+ make_row arg proof_conclusion
+
and andind conclude =
let module P = Mpresentation in
let module Con = Content in