Comments (5)
rlepigre
commented on August 16, 2024
Well, you should not be able to mix the legacy syntax with the actual lambdapi syntax. I'll check what I can do to reject the last two examples, and document the syntax properly.
from lambdapi.
rlepigre
commented on August 16, 2024
There is no bug here (any more?), only missing documentation. The first example uses the (correct) new syntax. The second example attempts to mix legacy syntax with new syntax, which is rejected at scoping type with an adequate error message (pointing to the position of the ?y[x] subterm). Finally, the last example is simply not syntactically correct: y[x] has no meaning in either the legacy and the new syntax.
from lambdapi.
francoisthire
commented on August 16, 2024
Maybe the file "newRuleSyntax.dk" should be renamed so that it is easier to understand that it is about Higher-Order patterns.
from lambdapi.
fblanqui
commented on August 16, 2024
@rlepigre : can't we close this issue?
from lambdapi.
rlepigre
commented on August 16, 2024
@fblanqui: I guess so.
from lambdapi.
Related Issues (20)
- Poor error message when a the proof end token is missing
- User shouldn't have to manually select Goal panel to see navigated goals
- Parsing failure prevents from showing log messages in debug terminal HOT 5
- unix library missing in dune
- Make commands systematically print an error when vscode isn't installed HOT 1
- Add a flag for (not) printing metavariable arguments
- Metavariable numbering not reset in each symbol/rule declaration HOT 2
- Add export to the new ARI format
- Could not declare symbol "-1" anymore HOT 3
- Add a lambdapi command dep to generate a Makefile to check files in parallel
- Reopen/navigate back the Goals and the console buffers when navigating proofs in Emacs
- In Emacs, the syntax error message at the end of a file, is not displayed in the console
- Fail to establishes physical links to the external symbols HOT 4
- Notations on external symbols are not exported
- Issue with the .xtc export of lambdapi files
- CI: build_vscode_extension failure HOT 2
- rewrite under quantifiers HOT 1
- Problem when killing LSP server in Emacs
- Emacs: goal not printed after begin or {
- make lambdapi available in opam on ppc64 arch
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from lambdapi.