Gaspard Férey

Declare injectivity on some arguments only

6

This seems to be a better place to discuss the following issue: Deducteam/Dedukti/issues/151 ### Problem Consider the following example encoding an `even` predicate on natural numbers: ``` // Encoding symbol...

The following file typechecks in less than one second in Dedukti 2.7 but is stuck in lambdapi when computing the second `#EVAL` command: ``` N : Type. z : N....

Rule name and priority

20

### Current state #### Names Right now a rule has a name that can be specified by the user using the syntax ``` {my_rule_name} [ctx] foo --> bar. ``` When...

Unjustified unsatisfiable constraint warning

5

Consider the following example ``` A : Type. def f : A -> A. B : A -> Type. consB : x : A -> B (f x). C :...

Implement schema patching (RFC 7386)

3

# Implements Schema patching This PR introduces schema patching, allowing fine-grained modifications to JSON schemas via a new `patchSchemaWith` key under `onyxia-api`, similar to overwriting. Schema resolution now supports [JSON...

I am not sure this branch should actually be merged since the orange template remains the default visual identity of Onyxia. This is a SSPCloud template then. Perhaps it belongs...

See #932 for context. This is suggestion 3. The configuration structure is naturally inherited from the `values.yaml` which is sometimes a bit too deeply hierarchical whereas forms are usually more...