Hi Michael,
Yes, Konrad's right about how types are determined in term quotations,
and I too don't know of an INST in HOL Light that unifies the types of
its arguments.
To get a listing of the types of the free variables in 'th', you can do:
map dest_var (frees th);;
or to return the type
Hi Michael,
What I think is happening is that each quoted element is being
parsed separately.
This means that the type of the x in `x` is a type variable while the type
of `2` is :num. Since INST (I think) just fails if the two types
aren't identical,
you get the displayed behaviour. There may w
The 2018 Alonzo Church Award for Outstanding
Contributions to Logic and Computation
Call for Nominations
Introduction
An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and
Computation, was established in 2015 by the ACM Special Interest Group
an example from the tutorial
let th1 = REFL `x+1`;;
val th1 : thm = |- x + 1 = x + 1
# let th3 = INST [`2`,`x:num`] th1;;
val th3 : thm = |- 2 + 1 = 2 + 1
Fine. But if we leave off the type information about x it doesn't work.
# let th3 = INST [`2`,`x`] th1;;
Warning: inventing type variabl
Dear HOL and Isabelle users,
If you are in LA for CPP, POPL etc., please consider attending a Monday (Jan.
8) morning POPL tutorial on recent advances with Isabelle/HOL’s codatatype and
corecursion infrastructure.
https://popl18.sigplan.org/track/POPL-2018-TutorialFest
http://andreipopescu.uk/
[Apologies if you receive multiple copies of this email. Please distribute to
interested parties.]
KR18 - Call for Tutorial and Workshop Proposals
** Apologies if you receive multiple copies of this call **
** Please distribute to interested parties **
C
FLoC 2018 — The 2018 Federated Logic Conference
6-19 July 2018
Oxford, England UK
http://www.floc2018.org/
In 1996, as part of its Special Year on Logic and Algorithms, DIMACS
hosted the first Federated Logic Conference (FLoC). It was modelled
after the successful Federated Computer Research Confe
34th International Conference on Logic Programming (ICLP 2018)
Call for Papers
=
July 14-17, 2018
Oxford, UK
http://www.logicprogramming.org/iclp2018
The 34th International Conference on Logic Programming (ICLP 2018) will take
place in Oxford, U.K. as part of FLO
