444 | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" |
444 | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" |
445 | _ => "Try this" |
445 | _ => "Try this" |
446 |
446 |
447 fun bunch_of_reconstructors needs_full_types lam_trans = |
447 fun bunch_of_reconstructors needs_full_types lam_trans = |
448 if needs_full_types then |
448 if needs_full_types then |
|
449 [Metis (full_type_enc, lam_trans false), |
|
450 Metis (really_full_type_enc, lam_trans false), |
|
451 Metis (full_type_enc, lam_trans true), |
|
452 Metis (really_full_type_enc, lam_trans true), |
|
453 SMT] |
|
454 else |
449 [Metis (partial_type_enc, lam_trans false), |
455 [Metis (partial_type_enc, lam_trans false), |
450 Metis (full_type_enc, lam_trans false), |
456 Metis (full_type_enc, lam_trans false), |
451 Metis (no_typesN, lam_trans true), |
457 Metis (no_typesN, lam_trans true), |
452 Metis (really_full_type_enc, lam_trans true), |
|
453 SMT] |
|
454 else |
|
455 [Metis (full_type_enc, lam_trans false), |
|
456 Metis (really_full_type_enc, lam_trans false), |
|
457 Metis (full_type_enc, lam_trans true), |
|
458 Metis (really_full_type_enc, lam_trans true), |
458 Metis (really_full_type_enc, lam_trans true), |
459 SMT] |
459 SMT] |
460 |
460 |
461 fun extract_reconstructor ({type_enc, lam_trans, ...} : params) |
461 fun extract_reconstructor ({type_enc, lam_trans, ...} : params) |
462 (Metis (type_enc', lam_trans')) = |
462 (Metis (type_enc', lam_trans')) = |