Logiweb(TM)

Logiweb aspects of premisecheck ( " , " ) in pyk

Up Help

The "pyk" aspect

Define pyk of premisecheck ( asterisk , asterisk ) as "premisecheck ( "! , "! )" end define

The "value" aspect

define value of premisecheck ( P , c ) as norm { P is val : { c is val : LET P ref BE { asterisk IN LET asterisk BE { r IN LET P idx BE { asterisk IN LET asterisk BE { i IN if c [[ r ]] [[ "diagnose" ]] != true then error ( P , diag ( "Lemma" ) disp ( P ) diag ( "occurs on a page with a non-empty diagnose." ) diag ( "Avoid referencing that lemma." ) end diagnose ) else if .not. checked ( r , c ) then error ( P , diag ( "Lemma" ) disp ( P ) diag ( "occurs on a page which has not been checked" ) diag ( "by the present proof checker." ) diag ( "Avoid referencing that lemma." ) end diagnose ) else if P proof-rhs ( c ) then error ( P , LocateProofLine ( P , c ) diag ( "Lemma" ) disp ( P ) diag ( "has no proof. Avoid referencing that lemma." ) end diagnose ) else true } } } } } } end define

The pyk compiler, version 0.1.9 by Klaus Grue,
GRD-2007-07-12.UTC:20:11:58.175987 = MJD-54293.TAI:20:12:31.175987 = LGT-4690987951175987e-6