Untersuchungsergebnis.mlg Download desLatech {Latech[59] Isabelle[133] Abap[215]}zum Wurzelverzeichnis wechseln
DECLARE PLUGIN "tuto3_plugin"
{
open Ltac_plugin
open Construction_game
(* This one is necessary, to avoid message about missing wit_string *)
open Stdarg
}
VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
| [ "Tuto3_1" ] ->
{ let env = Global.env () in
let sigma = Evd.from_env env in
let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in
let new_type_2 = EConstr.mkSort s in
let sigma, _ =
Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
Feedback.msg_notice
(Printer.pr_econstr_env env sigma new_type_2) }
END
VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
| [ "Tuto3_2" ] -> { example_sort_app_lambda () }
END
TACTIC EXTEND collapse_hyps
| [ "pack" "hypothesis" ident(i) ] ->
{ Tuto_tactic.pack_tactic i }
END
(* More advanced examples, where automatic proof happens but
no tactic is being called explicitly. The first one uses
type classes. *)
VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
| [ "Tuto3_3" int(n) ] -> { example_classes n }
END
(* The second one uses canonical structures. *)
VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
| [ "Tuto3_4" int(n) ] -> { example_canonical n }
END
[ zur Elbe Produktseite wechseln0.183Quellennavigators
]
