issues
search
Deducteam
/
Dedukti
Implementation of the λΠ-calculus modulo rewriting
https://deducteam.github.io
Other
198
stars
21
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
' not allowed at the beginning of an identifier
#328
fblanqui
opened
2 months ago
1
See that non-referenced test leads to failed CI
#327
GuillaumeGen
closed
7 months ago
0
Add check that all tests are mentionned in tests/main
#326
GuillaumeGen
closed
5 months ago
1
Fix #295
#325
GuillaumeGen
closed
5 months ago
2
Fix #318
#324
GuillaumeGen
closed
5 months ago
0
Fix #319
#323
GuillaumeGen
closed
3 months ago
3
parsing error
#322
fblanqui
opened
7 months ago
0
dk dep -s fails
#321
fblanqui
opened
7 months ago
0
dk --version doesn't work
#320
fblanqui
closed
7 months ago
1
a thm must have a type
#319
fblanqui
closed
3 months ago
0
dkcheck doesn't accept a rule LHS between parentheses
#318
fblanqui
closed
5 months ago
0
feature request: option for not printing warnings
#317
fblanqui
opened
10 months ago
2
Update tezt version
#316
GuillaumeGen
closed
8 months ago
4
Fix links
#315
GuillaumeGen
closed
9 months ago
1
Links seem to 404
#314
ice1000
closed
10 months ago
2
Pragmas pretty printing
#313
specialfish9
closed
11 months ago
0
Feature request: allowing local theorems
#312
fblanqui
opened
1 year ago
2
"Package conflict" when installing
#311
yoni206
closed
1 year ago
2
feature request: #REQUIRE module alias
#310
fblanqui
opened
1 year ago
0
Lexer: Fixes #308
#309
francoisthire
closed
1 year ago
0
Identifiers with single \ not accepted
#308
fblanqui
closed
1 year ago
0
More dks
#307
francoisthire
closed
1 year ago
0
Dkdep: Add a regression test for dkdep
#306
francoisthire
closed
1 year ago
0
Update dependencies
#305
francoisthire
closed
1 year ago
0
Dkdep: Make error message consistent
#304
francoisthire
closed
1 year ago
0
Erroneous suggestion from dk dep
#303
gabrielhdt
closed
1 year ago
1
Erroneous suggestion from dk dep
#302
gabrielhdt
closed
1 year ago
1
dk dep is too slow
#301
fblanqui
opened
1 year ago
0
dk --version does not work
#300
fblanqui
opened
1 year ago
0
Rules: Allow type annotations in higher-order patterns
#299
francoisthire
closed
1 year ago
5
Explicit require
#298
francoisthire
closed
1 year ago
0
Implement Dedukti standard
#297
francoisthire
closed
1 year ago
0
Fix filepath printing (fix #294)
#296
gabrielhdt
closed
1 year ago
0
Module identifier quoting
#295
gabrielhdt
closed
5 months ago
0
Path resolution
#294
gabrielhdt
closed
1 year ago
0
Rule typing failure
#293
gabrielhdt
opened
2 years ago
5
Francois@more tezt 3
#292
francoisthire
closed
2 years ago
0
Tests: Move more tests to Tezt
#291
francoisthire
closed
2 years ago
0
Move all the basic OK tests to Tezt
#290
francoisthire
closed
2 years ago
0
Functionalisation of dependencies
#289
francoisthire
closed
2 years ago
0
Importation is done before type checking
#288
francoisthire
opened
2 years ago
0
Introducing a toy example for the Dedukti's summer school
#287
francoisthire
closed
2 years ago
1
Command line manual is outdated
#286
francoisthire
opened
2 years ago
0
Parameters not allowed in the declaration of a definable symbol
#285
fblanqui
opened
2 years ago
0
Miscellaneous fixes
#284
gabrielhdt
closed
2 years ago
0
Pre Release 2.7
#283
gabrielhdt
closed
2 years ago
0
Add dependencies in dune-project
#282
gabrielhdt
closed
2 years ago
0
opam: Add missing dependencies
#281
francoisthire
closed
2 years ago
0
Kernel: Optimise conversion
#280
francoisthire
closed
2 years ago
1
Why Reduction.are_convertible_lst calls term_eq ?
#279
fblanqui
opened
2 years ago
5
Next