Skip to content

Commit

Permalink
Deploying to gh-pages from @ 00a2351 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@gares
gares committed Jun 10, 2024
1 parent 1ed0606 commit b13de2d
Show file tree
Hide file tree
Showing 5 changed files with 133 additions and 133 deletions.
30 changes: 15 additions & 15 deletions stlc.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,21 +119,21 @@ <h1>stlc.html</h1>
}
</script>
<p>Filter predicate: <input onkeyup='filter();' type='text' id='filter' name='filter'></p>
<div class='clause' predicate='declare-evar'><div class='loc'>File "coq-builtin.elpi: default-declare-evar", line 268, column 0, character 10808:</div><div class='hyps'>declare_constraint (declare-evar <span class='name' varname='1'>Ctx</span> <span class='name' varname='2'>RawEv</span> <span class='name' varname='3'>Ty</span> <span class='name' varname='4'>Ev</span>) <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='2'>RawEv</span></div><b>]</b></div></div><div class='concl'><div class='compound'>declare-evar <span class='name' varname='1'>Ctx</span> <span class='name' varname='2'>RawEv</span> <span class='name' varname='3'>Ty</span> <span class='name' varname='4'>Ev</span></div></div></div>
<div class='clause' predicate='rm-evar'><div class='loc'>File "coq-builtin.elpi", line 277, column 0, character 11168:</div><div class='hyps'><div class='hyp compound' level='60'>declare_constraint (rm-evar <span class='name' varname='5'>X</span> <span class='name' varname='6'>Y</span>) <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='5'>X</span><b>,</b></div><div class='compound'> <span class='name' varname='6'>Y</span></div><b>]</b></div></div></div><div class='concl neckcut'><div class='compound'>rm-evar <div class='compound'>(uvar&nbsp;<b>as</b>&nbsp;</div><div class='compound'><span class='name' varname='5'>X</span>)</div> <div class='compound'>(uvar&nbsp;<b>as</b>&nbsp;</div><div class='compound'><span class='name' varname='6'>Y</span>)</div></div></div></div>
<div class='clause' predicate='rm-evar'><div class='loc'>File "coq-builtin.elpi", line 278, column 0, character 11245:</div><div class='hyps'><div class='hyp'></div></div><div class='concl'>rm-evar _ _</div></div>
<div class='clause' predicate='evar'><div class='loc'>File "coq-builtin.elpi", line 299, column 0, character 12025:</div><div class='hyps'><div class='hyp compound' level='60'>var <span class='name' varname='9'>S</span> _ <span class='name' varname='10'>VL</span>,</div><div class='hyp compound'><span class='cut'>!</span>,</div><div class='hyp compound'>prune <span class='name' varname='8'>T</span> <span class='name' varname='10'>VL</span>,</div><div class='hyp compound'>prune <span class='name' varname='7'>X</span> <span class='name' varname='10'>VL</span>,</div><div class='hyp compound'>declare_constraint (evar <span class='name' varname='7'>X</span> <span class='name' varname='8'>T</span> <span class='name' varname='9'>S</span>) <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='7'>X</span><b>,</b></div><div class='compound'> <span class='name' varname='9'>S</span></div><b>]</b></div></div></div><div class='concl'><div class='compound'>evar <div class='compound'>(uvar&nbsp;<b>as</b>&nbsp;</div><div class='compound'><span class='name' varname='7'>X</span>)</div> <span class='name' varname='8'>T</span> <span class='name' varname='9'>S</span></div></div></div>
<div class='clause' predicate='evar'><div class='loc'>File "coq-builtin.elpi: default-assign-evar", line 302, column 0, character 12131:</div><div class='hyps'><div class='hyp'></div></div><div class='concl'>evar _ _ _</div></div>
<div class='clause' predicate='coq.env.const-opaque?'><div class='loc'>File "coq-builtin.elpi", line 747, column 3, character 30685:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.const-opaque use coq.env.opaque? in place of coq.env.const-opaque?,</div><div class='hyp compound'>coq.env.opaque? <span class='name' varname='11'>C</span></div></div><div class='concl'><div class='compound'>coq.env.const-opaque? <span class='name' varname='11'>C</span></div></div></div>
<div class='clause' predicate='coq.env.const-primitive?'><div class='loc'>File "coq-builtin.elpi", line 754, column 3, character 30933:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.const-primitive use coq.env.primitive? in place of coq.env.const-primitive?,</div><div class='hyp compound'>coq.env.primitive? <span class='name' varname='12'>C</span></div></div><div class='concl'><div class='compound'>coq.env.const-primitive? <span class='name' varname='12'>C</span></div></div></div>
<div class='clause' predicate='coq.env.begin-module'><div class='loc'>File "coq-builtin.elpi", line 835, column 0, character 34271:</div><div class='hyps'>coq.env.begin-module-functor <span class='name' varname='13'>Name</span> <span class='name' varname='14'>MP</span> []</div><div class='concl'><div class='compound'>coq.env.begin-module <span class='name' varname='13'>Name</span> <span class='name' varname='14'>MP</span></div></div></div>
<div class='clause' predicate='coq.env.begin-module-type'><div class='loc'>File "coq-builtin.elpi", line 848, column 0, character 34752:</div><div class='hyps'>coq.env.begin-module-type-functor <span class='name' varname='15'>Name</span> []</div><div class='concl'><div class='compound'>coq.env.begin-module-type <span class='name' varname='15'>Name</span></div></div></div>
<div class='clause' predicate='coq.CS.canonical-projections'><div class='loc'>File "coq-builtin.elpi", line 1211, column 0, character 48987:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.canonical-projections use coq.env.projections in place of coq.CS.canonical-projections,</div><div class='hyp compound'>coq.env.projections <span class='name' varname='16'>I</span> <span class='name' varname='17'>L</span></div></div><div class='concl'><div class='compound'>coq.CS.canonical-projections <span class='name' varname='16'>I</span> <span class='name' varname='17'>L</span></div></div></div>
<div class='clause' predicate='coq.reduction.cbv.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1514, column 0, character 61760:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.cbv-whd-all use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all,</div><div class='hyp compound'>coq.reduction.cbv.norm <span class='name' varname='18'>T</span> <span class='name' varname='19'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.cbv.whd_all <span class='name' varname='18'>T</span> <span class='name' varname='19'>R</span></div></div></div>
<div class='clause' predicate='coq.reduction.vm.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1521, column 0, character 62038:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.vm-whd-all use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all,</div><div class='hyp compound'>coq.reduction.vm.norm <span class='name' varname='20'>T</span> <span class='name' varname='21'>TY</span> <span class='name' varname='22'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.vm.whd_all <span class='name' varname='20'>T</span> <span class='name' varname='21'>TY</span> <span class='name' varname='22'>R</span></div></div></div>
<div class='clause' predicate='coq.reduction.lazy.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1528, column 0, character 62272:</div><div class='hyps'><div class='compound'>get-option coq:redflags coq.redflags.all&nbsp;<b>⇒</b>&nbsp;</div><div class='compound'>coq.reduction.lazy.whd <span class='name' varname='23'>X</span> <span class='name' varname='24'>Y</span></div></div><div class='concl'><div class='compound'>coq.reduction.lazy.whd_all <span class='name' varname='23'>X</span> <span class='name' varname='24'>Y</span></div></div></div>
<div class='clause' predicate='coq.id->name'><div class='loc'>File "coq-builtin.elpi", line 1645, column 0, character 66783:</div><div class='hyps'>coq.string-&gt;name <span class='name' varname='25'>S</span> <span class='name' varname='26'>N</span></div><div class='concl'><div class='compound'>coq.id-&gt;name <span class='name' varname='25'>S</span> <span class='name' varname='26'>N</span></div></div></div>
<div class='clause' predicate='coq.elpi.accumulate'><div class='loc'>File "coq-builtin.elpi", line 1746, column 0, character 70529:</div><div class='hyps'>coq.elpi.accumulate-clauses <span class='name' varname='27'>S</span> <span class='name' varname='28'>N</span> <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='29'>C</span></div><b>]</b></div></div><div class='concl'><div class='compound'>coq.elpi.accumulate <span class='name' varname='27'>S</span> <span class='name' varname='28'>N</span> <span class='name' varname='29'>C</span></div></div></div>
<div class='clause' predicate='declare-evar'><div class='loc'>File "coq-builtin.elpi: default-declare-evar", line 268, column 0, character 10807:</div><div class='hyps'>declare_constraint (declare-evar <span class='name' varname='1'>Ctx</span> <span class='name' varname='2'>RawEv</span> <span class='name' varname='3'>Ty</span> <span class='name' varname='4'>Ev</span>) <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='2'>RawEv</span></div><b>]</b></div></div><div class='concl'><div class='compound'>declare-evar <span class='name' varname='1'>Ctx</span> <span class='name' varname='2'>RawEv</span> <span class='name' varname='3'>Ty</span> <span class='name' varname='4'>Ev</span></div></div></div>
<div class='clause' predicate='rm-evar'><div class='loc'>File "coq-builtin.elpi", line 277, column 0, character 11167:</div><div class='hyps'><div class='hyp compound' level='60'>declare_constraint (rm-evar <span class='name' varname='5'>X</span> <span class='name' varname='6'>Y</span>) <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='5'>X</span><b>,</b></div><div class='compound'> <span class='name' varname='6'>Y</span></div><b>]</b></div></div></div><div class='concl neckcut'><div class='compound'>rm-evar <div class='compound'>(uvar&nbsp;<b>as</b>&nbsp;</div><div class='compound'><span class='name' varname='5'>X</span>)</div> <div class='compound'>(uvar&nbsp;<b>as</b>&nbsp;</div><div class='compound'><span class='name' varname='6'>Y</span>)</div></div></div></div>
<div class='clause' predicate='rm-evar'><div class='loc'>File "coq-builtin.elpi", line 278, column 0, character 11244:</div><div class='hyps'><div class='hyp'></div></div><div class='concl'>rm-evar _ _</div></div>
<div class='clause' predicate='evar'><div class='loc'>File "coq-builtin.elpi", line 299, column 0, character 12024:</div><div class='hyps'><div class='hyp compound' level='60'>var <span class='name' varname='9'>S</span> _ <span class='name' varname='10'>VL</span>,</div><div class='hyp compound'><span class='cut'>!</span>,</div><div class='hyp compound'>prune <span class='name' varname='8'>T</span> <span class='name' varname='10'>VL</span>,</div><div class='hyp compound'>prune <span class='name' varname='7'>X</span> <span class='name' varname='10'>VL</span>,</div><div class='hyp compound'>declare_constraint (evar <span class='name' varname='7'>X</span> <span class='name' varname='8'>T</span> <span class='name' varname='9'>S</span>) <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='7'>X</span><b>,</b></div><div class='compound'> <span class='name' varname='9'>S</span></div><b>]</b></div></div></div><div class='concl'><div class='compound'>evar <div class='compound'>(uvar&nbsp;<b>as</b>&nbsp;</div><div class='compound'><span class='name' varname='7'>X</span>)</div> <span class='name' varname='8'>T</span> <span class='name' varname='9'>S</span></div></div></div>
<div class='clause' predicate='evar'><div class='loc'>File "coq-builtin.elpi: default-assign-evar", line 302, column 0, character 12130:</div><div class='hyps'><div class='hyp'></div></div><div class='concl'>evar _ _ _</div></div>
<div class='clause' predicate='coq.env.const-opaque?'><div class='loc'>File "coq-builtin.elpi", line 747, column 3, character 30688:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.const-opaque use coq.env.opaque? in place of coq.env.const-opaque?,</div><div class='hyp compound'>coq.env.opaque? <span class='name' varname='11'>C</span></div></div><div class='concl'><div class='compound'>coq.env.const-opaque? <span class='name' varname='11'>C</span></div></div></div>
<div class='clause' predicate='coq.env.const-primitive?'><div class='loc'>File "coq-builtin.elpi", line 754, column 3, character 30936:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.const-primitive use coq.env.primitive? in place of coq.env.const-primitive?,</div><div class='hyp compound'>coq.env.primitive? <span class='name' varname='12'>C</span></div></div><div class='concl'><div class='compound'>coq.env.const-primitive? <span class='name' varname='12'>C</span></div></div></div>
<div class='clause' predicate='coq.env.begin-module'><div class='loc'>File "coq-builtin.elpi", line 835, column 0, character 34274:</div><div class='hyps'>coq.env.begin-module-functor <span class='name' varname='13'>Name</span> <span class='name' varname='14'>MP</span> []</div><div class='concl'><div class='compound'>coq.env.begin-module <span class='name' varname='13'>Name</span> <span class='name' varname='14'>MP</span></div></div></div>
<div class='clause' predicate='coq.env.begin-module-type'><div class='loc'>File "coq-builtin.elpi", line 848, column 0, character 34755:</div><div class='hyps'>coq.env.begin-module-type-functor <span class='name' varname='15'>Name</span> []</div><div class='concl'><div class='compound'>coq.env.begin-module-type <span class='name' varname='15'>Name</span></div></div></div>
<div class='clause' predicate='coq.CS.canonical-projections'><div class='loc'>File "coq-builtin.elpi", line 1211, column 0, character 48990:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.canonical-projections use coq.env.projections in place of coq.CS.canonical-projections,</div><div class='hyp compound'>coq.env.projections <span class='name' varname='16'>I</span> <span class='name' varname='17'>L</span></div></div><div class='concl'><div class='compound'>coq.CS.canonical-projections <span class='name' varname='16'>I</span> <span class='name' varname='17'>L</span></div></div></div>
<div class='clause' predicate='coq.reduction.cbv.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1514, column 0, character 61763:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.cbv-whd-all use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all,</div><div class='hyp compound'>coq.reduction.cbv.norm <span class='name' varname='18'>T</span> <span class='name' varname='19'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.cbv.whd_all <span class='name' varname='18'>T</span> <span class='name' varname='19'>R</span></div></div></div>
<div class='clause' predicate='coq.reduction.vm.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1521, column 0, character 62041:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.vm-whd-all use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all,</div><div class='hyp compound'>coq.reduction.vm.norm <span class='name' varname='20'>T</span> <span class='name' varname='21'>TY</span> <span class='name' varname='22'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.vm.whd_all <span class='name' varname='20'>T</span> <span class='name' varname='21'>TY</span> <span class='name' varname='22'>R</span></div></div></div>
<div class='clause' predicate='coq.reduction.lazy.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1528, column 0, character 62275:</div><div class='hyps'><div class='compound'>get-option coq:redflags coq.redflags.all&nbsp;<b>⇒</b>&nbsp;</div><div class='compound'>coq.reduction.lazy.whd <span class='name' varname='23'>X</span> <span class='name' varname='24'>Y</span></div></div><div class='concl'><div class='compound'>coq.reduction.lazy.whd_all <span class='name' varname='23'>X</span> <span class='name' varname='24'>Y</span></div></div></div>
<div class='clause' predicate='coq.id->name'><div class='loc'>File "coq-builtin.elpi", line 1645, column 0, character 66786:</div><div class='hyps'>coq.string-&gt;name <span class='name' varname='25'>S</span> <span class='name' varname='26'>N</span></div><div class='concl'><div class='compound'>coq.id-&gt;name <span class='name' varname='25'>S</span> <span class='name' varname='26'>N</span></div></div></div>
<div class='clause' predicate='coq.elpi.accumulate'><div class='loc'>File "coq-builtin.elpi", line 1746, column 0, character 70532:</div><div class='hyps'>coq.elpi.accumulate-clauses <span class='name' varname='27'>S</span> <span class='name' varname='28'>N</span> <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='29'>C</span></div><b>]</b></div></div><div class='concl'><div class='compound'>coq.elpi.accumulate <span class='name' varname='27'>S</span> <span class='name' varname='28'>N</span> <span class='name' varname='29'>C</span></div></div></div>
<div class='clause' predicate='true'><div class='loc'>File "elpi-builtin.elpi", line 9, column 0, character 89:</div><div class='hyps'><div class='hyp'></div></div><div class='concl'>true</div></div>
<div class='clause' predicate=';'><div class='loc'>File "elpi-builtin.elpi", line 28, column 0, character 296:</div><div class='hyps'><span class='name' varname='30'>A</span></div><div class='concl'><div class='compound'><div class='compound'>(<span class='name' varname='30'>A</span>&nbsp;;&nbsp;</div><div class='compound'>_)</div></div></div></div>
<div class='clause' predicate=';'><div class='loc'>File "elpi-builtin.elpi", line 30, column 0, character 311:</div><div class='hyps'><span class='name' varname='31'>B</span></div><div class='concl'><div class='compound'><div class='compound'>(_&nbsp;;&nbsp;</div><div class='compound'><span class='name' varname='31'>B</span>)</div></div></div></div>
Expand Down
Loading

0 comments on commit b13de2d

Please sign in to comment.