Commit a1c8c900 authored by g.genestier's avatar g.genestier

Add the file about the semantic of WHNF in Dedukti

parent be0b67aa
A : Type.
def g : A -> A.
def f : A -> A -> A.
def a : A.
def b : A.
[] g a --> f a b.
[] a --> b.
[x] f x x --> g x.
#EVAL[WHNF] (f a b).
(; retourne g a ;)
#EVAL[SNF] (f a b).
(; retourne g b ;)
(; retourne b ;)
\ 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