Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Recommited the changes for nitpick
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 28 Jan 2010 08:13:39 +0100
changeset 974 d44fda0cf393
parent 973 b582f7decd9a
child 977 07504636d14c
Recommited the changes for nitpick
Quot/quotient_term.ML file | annotate | diff | comparison | revisions 
--- a/Quot/quotient_term.ML	Wed Jan 27 18:26:01 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Jan 28 08:13:39 2010 +0100
@@ -14,6 +14,9 @@
   val absrep_fun: flag -> Proof.context -> typ * typ -> term
   val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
 
+  (* Allows Nitpick to represent quotient types as single elements from raw type *)
+  val absrep_const_chk: flag -> Proof.context -> string -> term
+
   val equiv_relation: Proof.context -> typ * typ -> term
   val equiv_relation_chk: Proof.context -> typ * typ -> term
 
@@ -133,6 +136,10 @@
   | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
 
+(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
+fun absrep_const_chk flag ctxt qty_str =
+  Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
+
 fun absrep_match_err ctxt ty_pat ty =
 let
   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
nominal2