Library nbe_tests
Require Import syntax.
Require Import nbe_cbv_atomic.
Parameter a:atoms.
Definition nbe_v := nbe_cbv_atomic.Completeness.NbE.
Check nbe_v.
Definition NbE {A} : proof nil false A -> bare := fun p => forget_proof (forget_nf (nbe_v p)).
Some tests of the normalization algorithm
Definition id8 : proof nil false (Func Nat (Func Nat Nat)).
Eval compute in (forget_proof id8).
Eval compute in (NbE id8).
Definition id9 : proof nil false (Func Nat Nat).
Eval compute in (forget_proof id9).
Eval compute in (NbE id9).
Definition id10 : proof nil false (Func Nat Nat).
Eval compute in (forget_proof id10).
Eval compute in (NbE id10).
Definition id11 : proof nil false (Func (Func Nat Nat) (Func Nat Nat)).
Eval compute in (forget_proof id11).
Eval compute in (NbE id11).
Definition id13 : proof nil false (Func (Func Nat Nat) (Func Nat Nat)).
Eval compute in (forget_proof id13).
Eval compute in (NbE id13).
Definition id14 : proof nil false (Func (Func Nat Nat) (Func Nat Nat)).
Eval compute in (forget_proof id14).
Eval compute in (NbE id14).
Definition id16 : proof nil false (Func (Func Nat Nat) (Func (Func Nat (Func Nat Nat)) (Func Nat Nat))).
Eval compute in (forget_proof id16).
Eval compute in (NbE id16).
Definition id19 : proof nil false
(Func (Func Nat Nat)
(Func (Func Nat Nat)
(Func (Func Nat Nat) (Func Nat Nat)))).
Eval compute in (forget_proof id19).
Eval compute in (NbE id19).
Definition id21 : proof nil false (Func (Sum Nat Nat) (Func Nat Nat)).
Eval compute in (forget_proof id21).
Eval vm_compute in (NbE id21).
Now some tests with numbers
Definition test22 : proof nil false Nat.
Eval compute in (forget_proof test22).
Eval compute in (NbE test22).
Definition test23 : proof nil false (Func Nat Nat).
Eval compute in (forget_proof test23).
Eval compute in (NbE test23).
Definition test24 : proof nil false (Func Nat Nat).
Eval compute in (forget_proof test24).
Eval compute in (NbE test24).
Definition test25 : proof nil false (Func Nat Nat).
Eval compute in (forget_proof test25).
Eval compute in (NbE test25).
Definition test26 : proof nil false (Func Nat (Func (Func Nat (Func Nat Nat)) Nat)).
This is blocking becaus A is a paramter, to investigate futher...
Eval compute in (forget_proof test26).
Eval compute in (NbE test26).
Definition test27 : proof nil false (Func Nat (Func (Func Nat (Func Nat Nat)) Nat)).
Eval compute in (forget_proof test27).
Eval compute in (NbE test27).
Definition test28 : proof nil false (Func Nat (Func (Func Nat (Func Nat Nat)) Nat)).
Eval compute in (forget_proof test28).
Eval compute in (NbE test28).
Definition test29 : proof nil false (Func Nat (Func (Func Nat (Func Nat Nat)) Nat)).
Eval compute in (forget_proof test29).
Eval compute in (NbE test29).
This page has been generated by coqdoc