Evgenii Balai
Evgenii Balai
E.g, this program: sorts # s = {a}. predicates p(#s). q(#s). rules p(a). q(a). # show p. When being run in SPARC with an option -A should only output p(a)...
Allow to use arithmetic expressions in definitions of a new constant, e.g: # const m = 1. # const n = m+1.
If a sparc program has many answer sets, they are all stored in a string buffer. This can be avioided by streaming them directly to the terminal window (when the...
Allow anonimous sorts (e.g, a predicate definition of the form p({a,b,c}).
Is there a way to obtain a callgraph in standalone mode? I tried to run the following: ``` evgenii@pop-os:~/Software/ccls/Release$ ccls '--init={"cache":{"directory":"/home/evgenii/ccls_project/.ccls_cache","retainInMemory":0},"compilationDatabaseDirectory":"/home/evgenii/ccls_project/","index":{"initialNoLinkage":false,"threads":10,"trackDependency":0}}' Content-Length: 225 {"jsonrpc":"2.0","method":"$ccls/call","params":{"textDocument":{"uri":"file:///home/evgenii/ccls_project/main.cpp"},"position":{"line":9,"character":8},"callee":false,"callType":3,"qualified":true,"hierarchy":true},"id":107} ``` But this returns an error:...
https://github.com/leanprover/theorem_proving_in_lean4/blob/ce23823e0e33bd153095dc307eae0341da2d9915/induction_and_recursion.md?plain=1#L684
https://github.com/leanprover/theorem_proving_in_lean4/blob/ce23823e0e33bd153095dc307eae0341da2d9915/tactics.md?plain=1#L122 C-c C-g seems to only work in lean3-mode: https://github.com/leanprover/lean3-mode lean4-mode uses C-c C-i instead: https://github.com/leanprover-community/lean4-mode I would delete this line or talk about C-c C-i instead.