proofpeer proofpeer-proofscript issues

proofpeer / proofpeer-proofscript

The language of ProofPeer: ProofScript

MIT License

8 stars 0 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Strange parsing in fresh quotes

#78 phlegmaticprogrammer closed 8 years ago
4
Comparison of contexts

#77 phlegmaticprogrammer closed 8 years ago
0
conversions should return theorems in current context

#76 phlegmaticprogrammer opened 8 years ago
3
Better naming for lifting canonically vs. structurally

#75 phlegmaticprogrammer closed 8 years ago
1
Implementing incontext, inliteralcontext, literalcontext

#74 phlegmaticprogrammer closed 8 years ago
0
Unicode symbol for function arrow

#73 phlegmaticprogrammer closed 8 years ago
1
Disallow tab character in ProofScript.

#72 phlegmaticprogrammer closed 8 years ago
1
Fix program level namespace resolution

#71 phlegmaticprogrammer closed 8 years ago
0
Lifting into completed context

#70 phlegmaticprogrammer closed 8 years ago
0
Introduce Literal Context

#69 phlegmaticprogrammer closed 8 years ago
0
Make logical namespace resolution a function of the context

#68 phlegmaticprogrammer closed 8 years ago
0
Main Context "Thread"

#67 phlegmaticprogrammer closed 8 years ago
0
fooJS/compile throws errors

#66 phlegmaticprogrammer opened 9 years ago
0
Parser throws exception

#65 ghost closed 9 years ago
1
Exception thrown for using type annotations of undefined type

#64 ghost opened 9 years ago
0
Term bug

#63 ghost closed 9 years ago
2
Custom datatypes in ProofScript

#62 phlegmaticprogrammer closed 9 years ago
13
Lifting terms

#61 ghost closed 9 years ago
2
root.thy is inconsistent.

#60 ghost closed 9 years ago
0
Lifting again

#59 ghost closed 9 years ago
1
Notion of goal

#58 phlegmaticprogrammer opened 9 years ago
0
Using bound variables in quotations

#57 phlegmaticprogrammer closed 9 years ago
1
Have "by" consume everything to the right

#56 ghost closed 9 years ago
0
ProofScript performance problem

#55 phlegmaticprogrammer closed 9 years ago
2
Inconsistent behaviour with table and def

#54 ghost closed 9 years ago
12
cached shows across theories

#53 ghost closed 9 years ago
4
Quotations in patterns for expressions

#52 phlegmaticprogrammer closed 9 years ago
1
Spurious error message for lists applied to (non-integer) values.

#51 ghost closed 9 years ago
0
Lifting

#50 ghost closed 9 years ago
1
Fully support types

#49 phlegmaticprogrammer closed 9 years ago
1
Required null check?

#48 ghost closed 9 years ago
0
Null exception

#47 ghost opened 9 years ago
0
Stackless ProofScript

#46 phlegmaticprogrammer closed 9 years ago
2
"Find an x such that ..." problems

#45 phlegmaticprogrammer opened 10 years ago
0
Odd behaviour of combine

#44 ghost closed 10 years ago
1
Context related problem reported by Phil in email

#43 phlegmaticprogrammer closed 10 years ago
1
Discrepancy getting quantified theorems from contexts

#42 ghost closed 9 years ago
15
Odd type-inference

#41 ghost closed 10 years ago
6
Abstraction

#40 ghost closed 10 years ago
5
sym for arbitrary type

#39 phlegmaticprogrammer closed 10 years ago
11
Style Guide

#38 phlegmaticprogrammer opened 10 years ago
9
Truncated whitespace on strings

#37 ghost closed 10 years ago
0
Cannot convert [] to string

#36 ghost closed 10 years ago
1
"java.util.NoSuchElementException: None.get"

#35 ghost closed 10 years ago
1
{ error printing } : Theorem when abusing (?) context objects?

#34 ghost closed 10 years ago
5
GC overhead limit exceeded when processing complex theory files

#33 ghost closed 10 years ago
12
Problems defining ABS_CONV

#32 ghost closed 10 years ago
4
Complaint of free variable using fresh variable short-hand

#31 ghost closed 10 years ago
5
Can't do simple matches

#30 ghost closed 10 years ago
5
Want to be able to keep hypotheses after lifting even if redundant

#29 ghost closed 10 years ago
1