-requires="helm-ng_disambiguation helm-lexicon helm-grafite_parser helm-tactics"
+requires="helm-ng_disambiguation helm-lexicon helm-grafite_parser helm-tactics helm-ng_paramodulation"
version="0.0.1"
archive(byte)="ng_tactics.cma"
archive(native)="ng_tactics.cmxa"
ng_refiner \
ng_disambiguation \
grafite_parser \
+ ng_paramodulation \
ng_tactics \
grafite_engine \
tptp_grafite \
gallina8Parser.cmi: types.cmo
grafiteParser.cmi: types.cmo
grafite.cmi: types.cmo
-engine.cmi:
-types.cmo:
-types.cmx:
-options.cmo:
-options.cmx:
gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmo gallina8Parser.cmi
| NLetIn of loc * npattern * CicNotationPt.term * string
| NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern
| NRewrite of loc * direction * CicNotationPt.term * npattern
+ | NAuto of loc * CicNotationPt.term auto_params
type ('term, 'lazy_term, 'reduction, 'ident) tactic =
(* Higher order tactics (i.e. tacticals) *)
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 21
+let magic = 22
type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
| NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
- | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> assert false
+ | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ | NAuto _ -> assert false
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
) hyps,
(text,prefix_len,concl))
) seqs)
+ | GrafiteAst.NAuto (_loc, params) ->
+ NTactics.auto_tac
+ ~params
| GrafiteAst.NCases (_loc, what, where) ->
NTactics.cases_tac
~what:(text,prefix_len,what)
SYMBOL <:unicode<vdash>>;
concl = tactic_term -> (List.rev hyps,concl) ] ->
G.NAssert (loc, seqs)
+ | IDENT "nauto"; params = auto_params -> G.NAuto (loc, params)
| IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
G.NCases (loc, what, where)
| IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
-terms.cmi:
pp.cmi: terms.cmi
founif.cmi: terms.cmi
index.cmi: terms.cmi
orderings.cmi: terms.cmi
-subst.cmi: terms.cmi
+fosubst.cmi: terms.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
terms.cmo: terms.cmi
terms.cmx: terms.cmi
pp.cmo: terms.cmi pp.cmi
pp.cmx: terms.cmx pp.cmi
-founif.cmo: terms.cmi subst.cmi founif.cmi
-founif.cmx: terms.cmx subst.cmx founif.cmi
+founif.cmo: terms.cmi fosubst.cmi founif.cmi
+founif.cmx: terms.cmx fosubst.cmx founif.cmi
index.cmo: terms.cmi index.cmi
index.cmx: terms.cmx index.cmi
orderings.cmo: terms.cmi orderings.cmi
orderings.cmx: terms.cmx orderings.cmi
-subst.cmo: terms.cmi subst.cmi
-subst.cmx: terms.cmx subst.cmi
+fosubst.cmo: terms.cmi fosubst.cmi
+fosubst.cmx: terms.cmx fosubst.cmi
nCicBlob.cmo: terms.cmi nCicBlob.cmi
nCicBlob.cmx: terms.cmx nCicBlob.cmi
cicBlob.cmo: terms.cmi cicBlob.cmi
cicBlob.cmx: terms.cmx cicBlob.cmi
+paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi founif.cmi paramod.cmi
+paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx founif.cmx paramod.cmi
PACKAGE = ng_paramodulation
INTERFACE_FILES = \
- terms.mli pp.mli founif.mli index.mli orderings.mli subst.mli \
- nCicBlob.mli cicBlob.mli
+ terms.mli pp.mli fosubst.mli founif.mli index.mli orderings.mli \
+ nCicBlob.mli cicBlob.mli paramod.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
let names = List.map (function Some (x,_) -> Some x | _ -> None) C.context;;
let pp t = CicPp.pp t names;;
+
+ let embed t = assert false;;
end
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+module Subst (B : Terms.Blob) = struct
+
+ let id_subst = [];;
+
+ let build_subst n t tail = (n,t) :: tail ;;
+
+ let rec lookup_subst var subst =
+ match var with
+ | Terms.Var i ->
+ (try
+ lookup_subst (List.assoc i subst) subst
+ with
+ Not_found -> var)
+ | _ -> var
+ ;;
+ let lookup_subst i subst = lookup_subst (Terms.Var i) subst;;
+
+ let is_in_subst i subst = List.mem_assoc i subst;;
+
+ (* filter out from metasenv the variables in substs *)
+ let filter subst varlist =
+ List.filter
+ (fun m ->
+ not (is_in_subst m subst))
+ varlist
+ ;;
+
+end
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+module Subst (B : Terms.Blob) :
+ sig
+ val id_subst : B.t Terms.substitution
+ val build_subst :
+ int -> B.t Terms.foterm -> B.t Terms.substitution ->
+ B.t Terms.substitution
+ val lookup_subst :
+ int -> B.t Terms.substitution -> B.t Terms.foterm
+ val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist
+ end
exception UnificationFailure of string Lazy.t;;
module Founif (B : Terms.Blob) = struct
- module Subst = Subst.Subst(B)
+ module Subst = Fosubst.Subst(B)
module U = Terms.Utils(B)
let unification vars locked_vars t1 t2 =
let rec aux arity = function
| Terms.Leaf a -> [Constant (a, arity)]
| Terms.Var i -> assert (arity = 0); [Variable]
- | Terms.Node (Terms.Var _::_) -> assert false
+ | Terms.Node (Terms.Var _::_) ->
+ (* FIXME : should this be allowed or not ? *)
+ assert false
| Terms.Node ([] | [ _ ] ) -> assert false
- | Terms.Node (Terms.Node _::_) -> assert false
+ | Terms.Node (Terms.Node _::_) -> assert false
| Terms.Node (hd::tl) ->
aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
in
(* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
-module type NCicContext =
+module type NCicContext =
sig
val metasenv : NCic.metasenv
val subst : NCic.substitution
let pp t =
NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
+ let rec embed = function
+ | NCic.Meta (i,_) -> Terms.Var i, [i]
+ | NCic.Appl l ->
+ let rec aux acc l = function
+ |[] -> acc@l
+ |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl
+ in
+ let res,vars = List.fold_left
+ (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
+ in (Terms.Node (List.rev res)), vars
+ | t -> Terms.Leaf t, []
+;;
+
end
--- /dev/null
+let nparamod metasenv subst context t =
+ let module C = struct
+ let metasenv = metasenv
+ let subst = subst
+ let context = context
+ end
+ in
+ let module B = NCicBlob.NCicBlob(C) in
+ let module Pp = Pp.Pp (B) in
+ let res,vars = B.embed t in
+ let module FU = Founif.Founif(B) in
+ let test_unification vars = function
+ | Terms.Node [_; _; lhs; rhs] ->
+ prerr_endline "Unification test :";
+ prerr_endline (Pp.pp_foterm lhs);
+ prerr_endline (Pp.pp_foterm rhs);
+ FU.unification vars [] lhs rhs
+ | _ -> assert false
+ in
+ let subst,vars = test_unification vars res in
+ prerr_endline "Result :";
+ prerr_endline (Pp.pp_foterm res);
+ prerr_endline "Substitution :";
+ prerr_endline (Pp.pp_substitution subst)
+;;
--- /dev/null
+val nparamod : NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> unit
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-module Subst (B : Terms.Blob) = struct
-
- let id_subst = [];;
-
- let build_subst n t tail = (n,t) :: tail ;;
-
- let rec lookup_subst var subst =
- match var with
- | Terms.Var i ->
- (try
- lookup_subst (List.assoc i subst) subst
- with
- Not_found -> var)
- | _ -> var
- ;;
- let lookup_subst i subst = lookup_subst (Terms.Var i) subst;;
-
- let is_in_subst i subst = List.mem_assoc i subst;;
-
- (* filter out from metasenv the variables in substs *)
- let filter subst varlist =
- List.filter
- (fun m ->
- not (is_in_subst m subst))
- varlist
- ;;
-
-end
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-
-module Subst (B : Terms.Blob) :
- sig
- val id_subst : B.t Terms.substitution
- val build_subst :
- int -> B.t Terms.foterm -> B.t Terms.substitution ->
- B.t Terms.substitution
- val lookup_subst :
- int -> B.t Terms.substitution -> B.t Terms.foterm
- val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist
- end
val eq : t -> t -> bool
val compare : t -> t -> int
val pp : t -> string
+ val embed : t -> t foterm * int list
end
module Utils (B : Blob) = struct
(* TODO: consider taking in input an imperative buffer for Format
* val pp : Format.formatter -> t -> unit
* *)
- val pp : t -> string
+ val pp : t -> string
+
+ val embed : t -> t foterm * int list
end
module Utils (B : Blob) :
[merge_tac])
) status
;;
+
+let auto ~params status goal =
+ let gty = get_goalty status goal in
+ let n,h,metasenv,subst,o = status.pstatus in
+ let status,t = term_of_cic_term status gty (ctx_of gty) in
+ Paramod.nparamod metasenv subst (ctx_of gty) t;
+ status
+;;
+
+let auto_tac ~params status =
+ distribute_tac (auto ~params) status
+;;
val assert_tac:
((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
NTacStatus.tactic
+
+val auto_tac:
+ params:'a -> NTacStatus.tactic
TPTP/Veloci/GRP595-1.p.ma logic/equality.ma
TPTP/Veloci/GRP570-1.p.ma logic/equality.ma
dependent_guarded_bove_capretta.ma nat/nat.ma
-TPTP/Veloci/SYN083-1.p.ma logic/equality.ma
interactive/test5.ma
+TPTP/Veloci/SYN083-1.p.ma logic/equality.ma
TPTP/Veloci/COL008-1.p.ma logic/equality.ma
TPTP/Veloci/GRP604-1.p.ma logic/equality.ma
record.ma
TPTP/Veloci/GRP612-1.p.ma logic/equality.ma
TPTP/Veloci/COL024-1.p.ma logic/equality.ma
TPTP/Veloci/GRP139-1.p.ma logic/equality.ma
-TPTP/Veloci/ROB010-1.p.ma logic/equality.ma
TPTP/Veloci/BOO006-2.p.ma logic/equality.ma
+TPTP/Veloci/ROB010-1.p.ma logic/equality.ma
TPTP/Veloci/LCL157-1.p.ma logic/equality.ma
TPTP/Veloci/LCL132-1.p.ma logic/equality.ma
constructor.ma coq.ma
TPTP/Veloci/LCL112-2.p.ma logic/equality.ma
formal_topology.ma logic/connectives.ma
TPTP/Veloci/RNG023-7.p.ma logic/equality.ma
-replace.ma coq.ma
test2.ma coq.ma
+replace.ma coq.ma
TPTP/Veloci/COL064-7.p.ma logic/equality.ma
TPTP/Veloci/BOO009-2.p.ma logic/equality.ma
TPTP/Veloci/GRP510-1.p.ma logic/equality.ma
TPTP/Veloci/GRP496-1.p.ma logic/equality.ma
TPTP/Veloci/COL084-1.p.ma logic/equality.ma
TPTP/Veloci/GRP174-1.p.ma logic/equality.ma
-TPTP/Veloci/RNG011-5.p.ma logic/equality.ma
TPTP/Veloci/GRP614-1.p.ma logic/equality.ma
+TPTP/Veloci/RNG011-5.p.ma logic/equality.ma
inversion.ma coq.ma
TPTP/Veloci/GRP592-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP182-1.p.ma logic/equality.ma
bad_tests/baseuri.ma
+TPTP/Veloci/GRP182-1.p.ma logic/equality.ma
TPTP/Veloci/GRP116-1.p.ma logic/equality.ma
coercions.ma nat/compare.ma nat/times.ma
TPTP/Veloci/GRP011-4.p.ma logic/equality.ma
TPTP/Veloci/GRP149-1.p.ma logic/equality.ma
TPTP/Veloci/COL013-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
TPTP/Veloci/COL064-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP567-1.p.ma logic/equality.ma
comments.ma coq.ma
TPTP/Veloci/COL021-1.p.ma logic/equality.ma
TPTP/Veloci/BOO006-4.p.ma logic/equality.ma
TPTP/Veloci/GRP545-1.p.ma logic/equality.ma
TPTP/Veloci/GRP520-1.p.ma logic/equality.ma
TPTP/Veloci/GRP457-1.p.ma logic/equality.ma
-TPTP/Veloci/BOO009-4.p.ma logic/equality.ma
TPTP/Veloci/COL064-9.p.ma logic/equality.ma
+TPTP/Veloci/BOO009-4.p.ma logic/equality.ma
TPTP/Veloci/LAT040-1.p.ma logic/equality.ma
TPTP/Veloci/GRP578-1.p.ma logic/equality.ma
change.ma coq.ma
ng_elim.ma ng_pts.ma
TPTP/Veloci/GRP597-1.p.ma logic/equality.ma
TPTP/Veloci/GRP572-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
TPTP/Veloci/GRP484-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP162-1.p.ma logic/equality.ma
fix_che_non_passa_ma_dovrebbe.ma list/list.ma nat/nat.ma
TPTP/Veloci/BOO011-4.p.ma logic/equality.ma
TPTP/Veloci/GRP580-1.p.ma logic/equality.ma
TPTP/Veloci/LCL134-1.p.ma logic/equality.ma
TPTP/Veloci/COL060-2.p.ma logic/equality.ma
TPTP/Veloci/BOO016-2.p.ma logic/equality.ma
-TPTP/Veloci/LAT039-2.p.ma logic/equality.ma
TPTP/Veloci/GRP542-1.p.ma logic/equality.ma
+TPTP/Veloci/LAT039-2.p.ma logic/equality.ma
+TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
TPTP/Veloci/GRP186-4.p.ma logic/equality.ma
TPTP/Veloci/GRP454-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP157-1.p.ma logic/equality.ma
TPTP/Veloci/GRP509-1.p.ma logic/equality.ma
TPTP/Veloci/GRP550-1.p.ma logic/equality.ma
ng_commands.ma nat/nat.ma ng_pts.ma
TPTP/Veloci/GRP487-1.p.ma logic/equality.ma
+paratest.ma nat/plus.ma
paramodulation/BOO075-1.ma
TPTP/Veloci/GRP605-1.p.ma logic/equality.ma
fguidi.ma logic/connectives.ma nat/nat.ma
TPTP/Veloci/GRP583-1.p.ma logic/equality.ma
TPTP/Veloci/GRP517-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
TPTP/Veloci/COL083-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP495-1.p.ma logic/equality.ma
TPTP/Veloci/GRP173-1.p.ma logic/equality.ma
coercions_propagation.ma logic/connectives.ma nat/orders.ma
TPTP/Veloci/LAT045-1.p.ma logic/equality.ma
-TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
TPTP/Veloci/GRP558-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP010-4.p.ma logic/equality.ma
interactive/test_instance.ma
TPTP/Veloci/COL012-1.p.ma logic/equality.ma
TPTP/Veloci/COL063-2.p.ma logic/equality.ma
TPTP/Veloci/RNG023-6.p.ma logic/equality.ma
color.ma logic/equality.ma nat/nat.ma
TPTP/Veloci/COL064-6.p.ma logic/equality.ma
-apply2.ma nat/nat.ma
metasenv_ordering.ma coq.ma
+apply2.ma nat/nat.ma
TPTP/Veloci/GRP608-1.p.ma logic/equality.ma
TPTP/Veloci/BOO010-2.p.ma logic/equality.ma
TPTP/Veloci/LCL153-1.p.ma logic/equality.ma
TPTP/Veloci/GRP552-1.p.ma logic/equality.ma
TPTP/Veloci/BOO013-2.p.ma logic/equality.ma
rewrite.ma coq.ma
-TPTP/Veloci/GRP497-1.p.ma logic/equality.ma
bad_tests/auto.ma coq.ma
+TPTP/Veloci/GRP497-1.p.ma logic/equality.ma
diabolic_fix.ma nat/nat.ma
TPTP/Veloci/GRP001-2.p.ma logic/equality.ma
test4.ma coq.ma
TPTP/Veloci/GRP514-1.p.ma logic/equality.ma
TPTP/Veloci/LCL139-1.p.ma logic/equality.ma
TPTP/Veloci/GRP547-1.p.ma logic/equality.ma
+TPTP/Veloci/COL004-3.p.ma logic/equality.ma
TPTP/Veloci/GRP459-1.p.ma logic/equality.ma
TPTP/Veloci/BOO069-1.p.ma logic/equality.ma
TPTP/Veloci/GRP137-1.p.ma logic/equality.ma
-TPTP/Veloci/COL004-3.p.ma logic/equality.ma
TPTP/Veloci/GRP188-2.p.ma logic/equality.ma
apply.ma coq.ma
TPTP/Veloci/GRP467-1.p.ma logic/equality.ma
TPTP/Veloci/COL063-4.p.ma logic/equality.ma
TPTP/Veloci/LCL155-1.p.ma logic/equality.ma
TPTP/Veloci/GRP588-1.p.ma logic/equality.ma
-lara.ma nat/nat.ma
TPTP/Veloci/GRP153-1.p.ma logic/equality.ma
paramodulation.ma coq.ma
TPTP/Veloci/GRP596-1.p.ma logic/equality.ma
TPTP/Veloci/GRP161-1.p.ma logic/equality.ma
TPTP/Veloci/COL064-8.p.ma logic/equality.ma
TPTP/Veloci/LDA001-1.p.ma logic/equality.ma
-TPTP/Veloci/COL050-1.p.ma logic/equality.ma
TPTP/Veloci/BOO010-4.p.ma logic/equality.ma
+TPTP/Veloci/COL050-1.p.ma logic/equality.ma
TPTP/Veloci/LCL110-2.p.ma logic/equality.ma
TPTP/Veloci/GRP491-1.p.ma logic/equality.ma
TPTP/Veloci/COL061-3.p.ma logic/equality.ma
compose.ma logic/equality.ma
TPTP/Veloci/COL025-1.p.ma logic/equality.ma
TPTP/Veloci/GRP115-1.p.ma logic/equality.ma
-hard_refine.ma coq.ma
letrecand.ma nat/nat.ma
unifhint.ma list/list.ma nat/nat.ma nat/plus.ma
+hard_refine.ma coq.ma
paramodulation/group.ma coq.ma
TPTP/Veloci/LCL158-1.p.ma logic/equality.ma
TPTP/Veloci/LCL133-1.p.ma logic/equality.ma
mysql_escaping.ma
TPTP/Veloci/LCL141-1.p.ma logic/equality.ma
TPTP/Veloci/GRP182-2.p.ma logic/equality.ma
-TPTP/Veloci/LDA007-3.p.ma logic/equality.ma
interactive/drop.ma
interactive/test6.ma
TPTP/Veloci/GRP599-1.p.ma logic/equality.ma
TPTP/Veloci/GRP574-1.p.ma logic/equality.ma
+TPTP/Veloci/LDA007-3.p.ma logic/equality.ma
unfold.ma coq.ma
TPTP/Veloci/GRP486-1.p.ma logic/equality.ma
TPTP/Veloci/GRP189-1.p.ma logic/equality.ma
match_inference.ma
simpl.ma coq.ma
unifhint_simple.ma logic/equality.ma
-TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
TPTP/Veloci/COL063-6.p.ma logic/equality.ma
+TPTP/Veloci/GRP142-1.p.ma logic/equality.ma
third.ma first.ma second.ma
TPTP/Veloci/GRP560-1.p.ma logic/equality.ma
TPTP/Veloci/GRP150-1.p.ma logic/equality.ma
TPTP/Veloci/GRP117-1.p.ma logic/equality.ma
multiple_inheritance.ma logic/equality.ma
test3.ma coq.ma
-TPTP/Veloci/GRP168-2.p.ma logic/equality.ma
TPTP/Veloci/ROB013-1.p.ma logic/equality.ma
+TPTP/Veloci/GRP168-2.p.ma logic/equality.ma
TPTP/Veloci/GRP012-4.p.ma logic/equality.ma
naiveparamod.ma logic/equality.ma
TPTP/Veloci/GRP176-2.p.ma logic/equality.ma
TPTP/Veloci/GRP458-1.p.ma logic/equality.ma
coercions_open.ma logic/equality.ma nat/nat.ma
paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma
-ng_uris_and_notation.ma nat/nat.ma
+ng_uris_and_notation.ma nat/nat.ma ng_pts.ma
TPTP/Veloci/GRP144-1.p.ma logic/equality.ma
TPTP/Veloci/BOO018-4.p.ma logic/equality.ma
TPTP/Veloci/LAT008-1.p.ma logic/equality.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "nat/plus.ma".
+
+ntheorem foo: \forall x, y. ((λz. x + x = z + z) ?).
+##[ #x; #y; nnormalize; nauto.
\ No newline at end of file
projects / helm.git / commitdiff