[opentheory-users] defineTypeOp underspecified? / opentheory be used as a proof verifier

[Günter Rote]

I am trying to write an article reader in python, mainly to
get an understanding how the steps of a formal proof in HOL look like.

My question concerns the definition of *defineTypeOp*
in the article file format
http://www.gilith.com/research/opentheory/article.html

Since the new constants *abs* and *rep*
appear in a term like "(⊦ (λa. abs (rep a)) = λa. a)",
they must have some type:

I guess the new type operator op with name n has
type parameters α1 ... αk in this order, and
the types of rep and abs are
 rep:: n α1 ... αk -> b
 abs:: b -> n α1 ... αk (using prefix notation for the type-operator)
where b is the type of t
Is that true?

In the definition of *opType*, is it required that
the length n of the list equals the k with which
the type-operator "op" has been defined?

(Maybe my question is based on a basic misunderstanding:
Can opentheory be used as a proof verifier?
I.e. If an article file goes through opentheory without
errors, does it mean that the listed "theorems" can be
derived from the "assumptions" (using the OpenTheory derivation rules)?

(I have seen talks about proof verification by transforming opentheory to
dedukti (or rather HOL via opentheory to dedukti) and then verifying the
proof in dedukti. What would be the point of this if this
verification is also fine in opentheory?)

-- 
G"unter Rote (Germany=49)30-838-75150 (office)
Freie Universit"at Berlin
Institut f"ur Informatik

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5311 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150806/7a016eed/attachment.bin>