Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Extra parameter for new_type command in nomdatatype allowing for mult…

…i-types.

Doesn't work unless each 'type' allows a 'VAR' constructor, which is not the case
in first order formulas and terms, for example.
  • Loading branch information...
commit 732b9f9e082d5475d0923eeec500d39d517d1875 1 parent decd84d
@mn200 mn200 authored
View
2  examples/lambda/barendregt/labelledTermsScript.sml
@@ -23,7 +23,7 @@ val lp = ``(λn (d:unit + unit + num) tns uns.
val {term_ABS_pseudo11, term_REP_11, genind_term_REP, genind_exists,
termP, absrep_id, repabs_pseudo_id, newty, term_REP_t, term_ABS_t,...} =
- new_type_step1 tyname {vp=vp, lp = lp}
+ new_type_step1 tyname 0 {vp=vp, lp = lp}
val _ = temp_overload_on ("termP", termP)
View
2  examples/lambda/basics/nomdatatype.sig
@@ -4,7 +4,7 @@ sig
include Abbrev
type coninfo = {con_termP : thm, con_def : thm}
- val new_type_step1 : string -> {vp:term,lp:term} ->
+ val new_type_step1 : string -> int -> {vp:term,lp:term} ->
{term_ABS_pseudo11 : thm,
term_REP_11 : thm,
term_REP_t : term,
View
5 examples/lambda/basics/nomdatatype.sml
@@ -116,9 +116,10 @@ fun first2 l =
(x::y::_) => (x,y)
| _ => raise Fail "first2: list doesn't have at least two elements"
-fun new_type_step1 tyname {vp, lp} = let
+fun new_type_step1 tyname n {vp, lp} = let
val list_mk_icomb = uncurry (List.foldl (mk_icomb o swap))
- val termP = list_mk_icomb (genind_t, [vp,lp,numSyntax.mk_numeral Arbnum.zero])
+ val termP =
+ list_mk_icomb (genind_t, [vp,lp,numSyntax.mk_numeral (Arbnum.fromInt n)])
fun termPf x = mk_comb(termP, x)
val (gtty,_) = dom_rng (type_of termP)
val x = mk_var("x",gtty) and y = mk_var("y", gtty)
View
2  examples/lambda/basics/termScript.sml
@@ -23,7 +23,7 @@ val lp = ``(λn (d:unit + unit) tns uns.
val {term_ABS_pseudo11, term_REP_11, genind_term_REP, genind_exists,
termP, absrep_id, repabs_pseudo_id, term_REP_t, term_ABS_t, newty, ...} =
- new_type_step1 tyname {vp=vp, lp = lp}
+ new_type_step1 tyname 0 {vp=vp, lp = lp}
val [gvar,glam] = genind_rules |> SPEC_ALL |> CONJUNCTS
val LAM_t = mk_var("LAM", ``:string -> ^newty -> ^newty``)
Please sign in to comment.
Something went wrong with that request. Please try again.