Repository navigation

Add lemmas to check the validity of extra rules - #77

Merged

fblanqui merged 17 commits into

Deducteam:masterfrom

Oct 2, 2026

Merged

Add lemmas to check the validity of extra rules#77
fblanqui merged 17 commits into
Deducteam:masterfrom
fblanqui:extra

Commits on Sep 29, 2026
- Add lemmas and definitions from Alethe development
  NotBad4U
  committed
  ada38d0
- Fix all comment of PR review
  NotBad4U
  committed
  3e45885
- Update mergesort and fix coprod deps
  NotBad4U
  committed
  360919a
Commits on Oct 1, 2026
- remove useless require
  fblanqui
  committed
  16d8eb7
- CHANGES: record only changes wrt previous release
  fblanqui
  committed
  c35c950
- remove useless requires
  fblanqui
  committed
  02cef9a
- remove useless explicit arguments
  fblanqui
  committed
  32041cc
- moved relation between sum and prod at the end
  fblanqui
  committed
  7afda8c
- derive ProdExt by defining Prod inductively
  fblanqui
  committed
  42735f1
- update CHANGES
  fblanqui
  committed
  2b684cb
Commits on Oct 2, 2026
- details
  fblanqui
  committed
  8f293f1
- details
  fblanqui
  committed
  c8a10c5
- details
  fblanqui
  committed
  496c0fa
- add lemmas to check the validity of extra rules
  fblanqui
  committed
  e10fb36
- Merge remote-tracking branch 'dk/master' into extra
  fblanqui
  committed
  d1cf7fd
- wip
  fblanqui
  committed
  881368a
- wip
  fblanqui
  committed
  7342490