search

JacquesCarette / hol-light-qe

The HOL Light theorem prover (moved from Google code)
Other
7 stars 1 forks source link

isConstruction #8

Closed laskowsp closed 4 years ago

laskowsp commented 7 years ago

I have currently defined isConstruction as:

let isConstruction = define `
(isConstruction (QuoVar str ty) = T) /\ 
(isConstruction (QuoConst str ty) = T) /\
(isConstruction (App exp1 exp2) = ((isConstruction exp1) /\ (isConstruction (exp2)))) /\
(isConstruction (Abs exp1 exp2) = ((isConstruction exp1) /\ (isConstruction exp2))) /\
(isConstruction (Quo exp1) = (isConstruction exp1)) 
`;;

This means that while it should return true when the term is a construction, it will never return false, and so something like isConstruction ((f x):epsilon) will just be unprovable instead of returning a definite result. Is this alright?

JacquesCarette commented 4 years ago

This old issue should get resolved, one way or another.

wmfarmer commented 4 years ago

I think the definition of isConstruction is fine for now. So I am going to close this issue.