Commit 4a430264 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Commentaire explicite sur le refus de la terminaison de stt

parent 912d3677
......@@ -20,11 +20,11 @@ def eps : eta prop -> Type.
[l, r] eps (impl l r) --> eps l -> eps r.
(; Rien n'interdit d'ajouter un jour
(; Rien n'interdit d'ajouter un jour, ce qui justifie de refuser la règle eps (forall A f)
e : type.
def phi : eta e -> eta prop.
[x] phi x --> forall e phi.
(; ;)
\ No newline at end of file
(; Cette règle est terminante et ne fait aucun appel à eps, donc est entièrement disjointe de la règle eps (forall A f) dans le call graph ;)
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment