Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
Overview
Comment:  Fixed demo IH to conform to the new verticalbar encoding. 

Downloads:  Tarball  ZIP archive  SQL archive 
Timelines:  family  ancestors  descendants  both  trunk 
Files:  files  file ages  folders 
SHA1:  925c93ea0ac1059125ed5184e3ab9ba93adf127e 
User & Date:  andy 20150416 22:01:04 
Context
20150416
 
22:02  Fixed many small bugs in elaboration, checking of incomplete proofs. checkin: 6ca1a452f3 user: andy tags: trunk  
22:01  Fixed demo IH to conform to the new verticalbar encoding. checkin: 925c93ea0a user: andy tags: trunk  
22:00  Fixed a bug in merging of substitutions with some arguments unbound. checkin: acfcbdeb7a user: andy tags: trunk  
Changes
Changes to plsrc/nat_spec_demo.pl.
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 
spec([
% Due to an oversight on my part, the way we handle inductive proofs,
% although correct, will not work with the kind of incremental proofs
% construction we are aiming to do. More permanent solutions will have to
% come later, but for now we hardcode the IH into the specification.
% (Which, yes, means that you can only prove one thing by induction!)
ih('IH', add(' x', z, ' x'), 'nat\\sml'(' x')),
% Nat formation rules
rule('Natz', nat(z), and([true])),
rule('Natsucc', nat(s(' n')), and([nat(' n')])),
% Addition rules
rule('Addz', add(z,' x', ' x'), and([true])),

 
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 
spec([
% Due to an oversight on my part, the way we handle inductive proofs,
% although correct, will not work with the kind of incremental proofs
% construction we are aiming to do. More permanent solutions will have to
% come later, but for now we hardcode the IH into the specification.
% (Which, yes, means that you can only prove one thing by induction!)
ih('IH', add(' x', z, ' x'), 'natsml'(' x')),
% Nat formation rules
rule('Natz', nat(z), and([true])),
rule('Natsucc', nat(s(' n')), and([nat(' n')])),
% Addition rules
rule('Addz', add(z,' x', ' x'), and([true])),
