Commit bce92954 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

6nov rule need itself to type-check (in KO repo)

parent 7eb85198
A : Type.
a : A.
b : A.
def T : A -> Type.
def C : (x : A) -> T x -> Type.
[] C b _ --> A.
(; This rule needs itself to type-check, since a must be in T b,
which is true if T b --> C b a --> A but not without any rule to define T ;)
[] T b --> C b a.
Nat : Type.
def S : Nat -> Nat.
omega : Nat.
[] S omega --> omega.
def Term : Nat -> Type.
[x] Term (S x) --> Nat -> Term x -> Term x.
def delta : (a : Nat) -> Term (S a) -> Term a.
[f] delta omega f --> f omega f.
\ No newline at end of file
nat : Type.
0 : nat.
S : nat -> nat.
def F0 : nat -> nat -> nat.
def F : nat -> nat -> nat.
def ack : nat -> nat -> nat.
[] F 0 --> S.
[n] F (S n) --> m : nat => F0 n m.
[n1] F0 n1 0 --> F n1 (S 0).
[n1,n3] F0 n1 (S n3) --> F n1 (F0 n1 n3).
[n] ack n --> F n.
def 4 := S (S (S (S 0))).
def OMEGA : nat := ack 4 4.
def f (x : nat) := x.
def g (x : nat) := x.
#ASSERT OMEGA == OMEGA.
#EVAL[WHNF,1] f OMEGA.
#EVAL[WHNF,2] f OMEGA.
(; TOO SLOW ;)
(; #EVAL[WHNF] f OMEGA. ;)
(; #ASSERT f OMEGA == OMEGA. ;)
\ No newline at end of file
(; Types ;)
t : Type.
(; Constructors ;)
True : t.
False : t.
(; Many functions ;)
def not : t -> t.
[] not True --> False.
[] not False --> True.
def equalt : t -> t -> t.
[] equalt True True --> True
[] equalt True False --> False
[] equalt False True --> False
[] equalt False False --> True.
def and : t -> t -> t.
[] and False _ --> False
[] and _ False --> False
[] and True True --> True.
def or : t -> t -> t.
[] or True _ --> True
[] or _ True --> True
[] or False False --> False.
def impli : t -> t -> t := (x => y => or (not x) y).
#REQUIRE Bool.
(; Type ;)
t : Type.
(; Constructors ;)
0 : t.
S : t -> t.
(; Many functions ;)
def pred : t -> t.
[n] pred (S n) --> n.
def plus : t -> t -> t.
[n] plus 0 n --> n
[m, n] plus (S m) n --> S (plus m n)
[n] plus n 0 --> n
[m, n] plus m (S n) --> S (plus m n).
def plus_rec_term : t -> t -> t.
[n] plus_rec_term 0 n --> n
[m, n] plus_rec_term (S m) n --> plus_rec_term m (S n).
def mult : t -> t -> t.
[] mult 0 _ --> 0
[m, n] mult (S m) n --> plus n (mult m n).
def even : t -> Bool.t.
[] even 0 --> Bool.True.
[n] even (S n) --> Bool.not (even n).
def odd : t -> Bool.t.
[] odd 0 --> Bool.True.
[n] odd (S n) --> Bool.not (odd n).
def even_rec_term : t -> Bool.t.
def odd_rec_term : t -> Bool.t.
[] even_rec_term 0 --> Bool.True.
[] odd_rec_term 0 --> Bool.True.
[n] even_rec_term (S n) --> odd_rec_term n.
[n] odd_rec_term (S n) --> even_rec_term n.
def equal : t -> t -> Bool.t.
[] equal 0 0 --> Bool.True
[] equal (S _) 0 --> Bool.False
[] equal 0 (S _) --> Bool.False
[m,n] equal (S m) (S n) --> equal m n.
def leq : t -> t -> Bool.t.
[] leq 0 _ --> Bool.True
[m] leq (S m) 0 --> Bool.False
[m, n] leq (S m) (S n) --> leq m n.
def moitie : t -> t.
[] moitie 0 --> 0
[n] moitie (S (S n)) --> S (moitie n).
def double_add : t -> t.
[n] double_add n --> plus n n.
def double_mult : t -> t.
[n] double_mult n --> mult (S (S 0)) n.
def double_constr : t -> t.
[] double_constr 0 --> 0
[n] double_constr (S n) --> S (S (double_constr n)).
def Ackermann : t -> t -> t.
[n] Ackermann 0 n --> S n
[m] Ackermann (S m) 0 --> Ackermann m (S 0)
[m, n] Ackermann (S m) (S n) --> Ackermann m (Ackermann (S m) n).
def factorielle : t -> t.
[] factorielle 0 --> S 0.
[n] factorielle (S n) --> mult (S n) (factorielle n).
......@@ -13,7 +13,7 @@ def f : Nat -> Nat -> Nat.
[x,y] f (double x) y --> S (S (S (S (S 0)))).
[x,y,z] f (plus x y) z --> S (S (S (S 0))).
[x,y] f (S (S x)) 0 --> 0.
[x] f (S (S x)) 0 --> 0.
[x,y] f x (S y) --> S 0.
[x,y] f (S (S x)) (S y) --> S (S (S 0)).
......@@ -21,11 +21,10 @@ def f : Nat -> Nat -> Nat.
#EVAL (f (S (S 0)) (S (S 0))).
def eq : Nat -> Nat -> Nat.
[x] eq x x --> S 0.
[x] eq x x --> S 0.
[x,y] eq x y --> 0.
def e := x : Nat => y : Nat => (eq x y).
#EVAL[WHNF] e.
#EVAL[HNF] e.
#EVAL[SNF] e.
Nat : Type.
z : Nat.
s : Nat -> Nat.
True : Type.
I : True.
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
def cumul : Sort -> Sort -> Type.
[s] cumul prop s --> True.
[i] cumul (type z) (type i) --> True.
[i,j] cumul (type (s i)) (type (s j)) --> cumul (type i) (type j).
(; Universe successors ;)
def succ : Sort -> Sort.
[] succ prop --> type z.
[i] succ (type i) --> type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[s1] rule s1 prop --> prop.
[i] rule (type i) (type z) --> type i.
[i, j] rule (type (s i)) (type (s j)) --> succ (rule (type i) (type j)).
(; Types and terms ;)
Univ : s : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (succ s).
private def lift' : s1 : Sort -> s2 : Sort -> Univ s1 -> Univ s2.
def lift : s1 : Sort -> s2 : Sort -> cumul s1 s2 -> a : Univ s1 -> Univ s2.
[s1,s2] lift s1 s2 _ --> lift' s1 s2.
def prod : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : (Term s1 a -> Univ s2) -> Univ (rule s1 s2).
[s] Term _ (univ s) --> Univ s.
[s1, s2, a] Term _ (lift' s1 s2 a) --> Term s1 a.
[s1, s2, a, b]
Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
[s, a] lift' s s a --> a.
[s1, s2, s3, a] lift' _ s3 (lift' s1 s2 a) --> lift' s1 s3 a.
[s1, s2, s3, a,b]
prod _ s2 (lift' s1 s3 a) b -->
lift' (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
[s1, s2, s3, a,b]
prod s1 _ a (x => lift' s2 s3 (b x)) -->
lift' (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
bool : Type.
term : Type.
def if : bool -> term -> term -> term.
[a,b,TT,TF,F] if a (if b TT TF) F --> if b (if a TT F) (if a TF F).
\ No newline at end of file
Nat : Type.
z : Nat.
s : Nat -> Nat.
def m : Nat -> Nat -> Nat.
[i] m i z --> i.
[j] m z j --> j.
[i, j] m (s i) (s j) --> s (m i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
(; Universe successors ;)
def succ : Sort -> Sort.
[] succ prop --> type z.
[i] succ (type i) --> type (s i).
def rule : Sort -> Sort -> Sort.
[s1] rule s1 prop --> prop.
[s2] rule prop s2 --> s2.
[i, j] rule (type i) (type j) --> type (m i j).
def max : Sort -> Sort -> Sort.
[s1] max s1 prop --> s1.
[s2] max prop s2 --> s2.
[i, j] max (type i) (type j) --> type (m i j).
[s] max s s --> s.
[s1,s2] succ (max s1 s2) --> max (succ s1) (succ s2).
[s1,s2,s3] max (max s1 s2) s3 --> max s1 (max s2 s3).
[s1,s2,s3] rule s1 (max s2 s3) --> max (rule s1 s2) (rule s1 s3).
[s1,s2,s3] rule (max s1 s2) s3 --> max (rule s1 s3) (rule s2 s3).
def ?0 : Sort.
def ?1 : Sort.
def ?2 : Sort.
def ?3 : Sort.
def ?4 : Sort.
def ?5 : Sort.
def ?6 : Sort.
def ?7 : Sort.
def ?8 : Sort.
def ?9 : Sort.
def ?10 : Sort.
[] ?1 --> succ ?3.
[] ?3 --> ?10.
[] ?4 --> ?10.
[] ?9 --> ?10.
[] ?6 --> ?10.
[] ?8 --> ?10.
[] ?7 --> type z.
[] ?5 --> max ?10 (type z).
[] max ?10 (type z) --> rule ?10 (type z).
[] ?2 --> rule ?10 (rule ?10 (type z)).
[] ?0 --> rule (succ ?10) (rule ?10 (rule ?10 (type z))).
def ?23996 : Sort.
def ?23997 : Sort.
def ?23998 : Sort.
def ?23999 : Sort.
def ?24000 : Sort.
def ?24001 : Sort.
def ?24002 : Sort.
def ?24003 : Sort.
def ?24004 : Sort.
def ?24005 : Sort.
def ?24006 : Sort.
def ?24007 : Sort.
def ?24008 : Sort.
def ?24009 : Sort.
def ?24010 : Sort.
def ?24011 : Sort.
def ?24012 : Sort.
def ?24013 : Sort.
def ?24014 : Sort.
def ?24015 : Sort.
def ?24016 : Sort.
def ?24017 : Sort.
def ?24018 : Sort.
def ?24019 : Sort.
def ?24020 : Sort.
def ?24021 : Sort.
def ?24022 : Sort.
def ?24023 : Sort.
def ?24943 : Sort.
def ?24944 : Sort.
def ?24945 : Sort.
def ?24946 : Sort.
def ?24947 : Sort.
def ?24948 : Sort.
def ?24949 : Sort.
def ?24950 : Sort.
def ?24951 : Sort.
def ?24952 : Sort.
def ?24953 : Sort.
def ?24954 : Sort.
def ?24955 : Sort.
def ?24956 : Sort.
def ?24957 : Sort.
def ?24958 : Sort.
def ?24959 : Sort.
def ?24960 : Sort.
def ?24961 : Sort.
def ?24962 : Sort.
def ?24963 : Sort.
def ?24964 : Sort.
def ?24965 : Sort.
def ?24966 : Sort.
def ?24967 : Sort.
def ?24968 : Sort.
def ?24969 : Sort.
def ?24970 : Sort.
def ?24971 : Sort.
def ?24972 : Sort.
def ?24973 : Sort.
def ?24974 : Sort.
def ?30 : Sort.
def ?31 : Sort.
def ?32 : Sort.
def ?33 : Sort.
def ?34 : Sort.
[] ?10 --> max ?24945 (max ?24946 ?24004).
[] ?24943 --> succ ?24945.
[] ?24944 --> succ ?24946.
[] ?23998 --> max ?24945 ?24946.
[] ?24001 --> succ ?24003.
[] ?24002 --> succ ?24004.
[] ?24006 --> succ ?24008.
[] ?24007 --> succ ?24009.
[] ?24008 --> max ?24945 ?24946.
[] ?24003 --> max ?24945 ?24946.
[] ?24010 --> max ?24945 ?24946.
[] ?24004 --> ?24009.
[] ?24000 --> succ ?24005.
[] ?23999 --> succ ?24005.
[] max ?24945 (max ?24946 ?24004) --> max ?24945 (max ?24946 ?24009).
[] ?23996 --> max (rule ?24945 (succ ?24005)) (rule ?24946 ?24005).
[] max (rule ?24945 (succ ?24005)) (rule ?24946 ?24005) -->
max (rule ?24945 (succ ?24005)) (rule ?24946 (succ ?24005)).
[] ?24011 --> max ?24945 ?24946.
[] ?24023 --> max ?24945 ?24946.
[] ?24014 --> succ ?24016.
[] ?24015 --> succ ?24017.
[] ?24016 --> max ?24945 ?24946.
[] max ?24945 (max ?24946 ?24009) --> max ?24945 (max ?24946 ?24017).
[] ?24019 --> succ ?24021.
[] ?24020 --> succ ?24022.
[] ?24021 --> max ?24945 ?24946.
[] max ?24945 (max ?24946 ?24017) --> max ?24945 (max ?24946 ?24022).
[] ?24017 --> ?24022.
[] ?24013 --> succ ?24018.
[] ?24012 --> succ ?24018.
[] ?23997 --> max (rule ?24945 (succ ?24018)) (rule ?24946 (succ ?24018)).
[] ?24949 --> ?24945.
[] ?24945 --> ?24961.
[] max (rule ?24961 (succ ?24005)) (rule ?24946 ?24005) -->
max (rule ?24961 (succ ?24005)) (rule ?24946 (succ ?24005)).
[] max ?24961 (max ?24946 ?24009) --> max ?24961 (max ?24946 ?24022).
[] ?24952 --> succ ?24954.
[] ?24953 --> succ ?24955.
[] ?24954 --> ?24961.
[] max ?24961 (max ?24946 ?24022) --> max ?24961 ?24955.
[] ?24957 --> succ ?24959.
[] ?24958 --> succ ?24960.
[] ?24959 --> ?24961.
[] max ?24961 ?24955 --> max ?24961 ?24960.
[] ?24955 --> ?24960.
[] ?24950 --> succ ?24956.
[] ?24951 --> succ ?24956.
[] ?24947 --> rule ?24961 ?24956.
[] rule ?24961 ?24956 --> rule ?24961 (succ ?24956).
[] ?24962 --> ?24961.
[] ?24974 --> ?24961.
[] ?24965 --> succ ?24967.
[] ?24966 --> succ ?24968.
[] ?24967 --> ?24961.
[] max ?24961 ?24960 --> max ?24961 ?24968.
[] ?24970 --> succ ?24972.
[] ?24971 --> succ ?24973.
[] ?24972 --> ?24961.
[] max ?24961 ?24968 --> max ?24961 ?24973.
[] ?24968 --> ?24973.
[] ?24964 --> succ ?24969.
[] ?24963 --> succ ?24969.
[] ?24948 --> rule ?24961 (succ ?24969).
[] ?24960 --> ?24973.
[] ?34 --> ?24956.
[] ?33 --> ?24973.
[] ?32 --> succ ?34.
[] ?31 --> succ ?34.
[] ?30 --> rule ?24961 ?34.
[] rule ?24961 ?34 --> rule ?24961 (succ ?34).
[] max (succ ?24946) (succ ?24009) --> succ ?24973.
[] max ?24946 ?24009 --> ?24973.
[] ?24005 --> max ?24956 ?24969.
[] max (rule ?24961 (succ ?24969)) (max (rule ?24946 ?24956) (rule ?24946 ?24969)) -->
max (rule ?24946 (succ ?24956)) (max (rule ?24961 (succ ?24969)) (rule ?24946 (succ ?24969))).
\ No newline at end of file
#REQUIRE natBinaire.
Int : Type.
def Nat := natBinaire.Nat.
......
......@@ -2,6 +2,8 @@
(; Nat as first order terms ;)
(;-------------------------------------------;)
#REQUIRE firstOrder.
def N := firstOrder.Term.
0 : N.
......
#REQUIRE Nat.
Figure : Type.
0 : Figure.
1 : Figure.
......@@ -20,55 +22,55 @@ Number : Type.
Zero : Number.
Cons : Number -> Figure -> Number.
def decimal : tuto.Nat -> Number.
def decimal_aux : tuto.Nat -> Number -> Number.
def decimal : Nat.t -> Number.
def decimal_aux : Nat.t -> Number -> Number.
[n] decimal n --> decimal_aux n Zero.
[N] decimal_aux tuto.0 N --> N.
[n] decimal_aux (tuto.S n) Zero --> decimal_aux n (Cons Zero 1).
[n,N] decimal_aux (tuto.S n) (Cons N 0) --> decimal_aux n (Cons N 1).
[n,N] decimal_aux (tuto.S n) (Cons N 1) --> decimal_aux n (Cons N 2).
[n,N] decimal_aux (tuto.S n) (Cons N 2) --> decimal_aux n (Cons N 3).
[n,N] decimal_aux (tuto.S n) (Cons N 3) --> decimal_aux n (Cons N 4).
[n,N] decimal_aux (tuto.S n) (Cons N 4) --> decimal_aux n (Cons N 5).
[n,N] decimal_aux (tuto.S n) (Cons N 5) --> decimal_aux n (Cons N 6).
[n,N] decimal_aux (tuto.S n) (Cons N 6) --> decimal_aux n (Cons N 7).
[n,N] decimal_aux (tuto.S n) (Cons N 7) --> decimal_aux n (Cons N 8).
[n,N] decimal_aux (tuto.S n) (Cons N 8) --> decimal_aux n (Cons N 9).
[n,N] decimal_aux (tuto.S n) (Cons N 9) --> decimal_aux n (Cons (decimal_aux (tuto.S tuto.0) N) 0).
[N] decimal_aux Nat.0 N --> N.
[n] decimal_aux (Nat.S n) Zero --> decimal_aux n (Cons Zero 1).
[n,N] decimal_aux (Nat.S n) (Cons N 0) --> decimal_aux n (Cons N 1).
[n,N] decimal_aux (Nat.S n) (Cons N 1) --> decimal_aux n (Cons N 2).
[n,N] decimal_aux (Nat.S n) (Cons N 2) --> decimal_aux n (Cons N 3).
[n,N] decimal_aux (Nat.S n) (Cons N 3) --> decimal_aux n (Cons N 4).
[n,N] decimal_aux (Nat.S n) (Cons N 4) --> decimal_aux n (Cons N 5).
[n,N] decimal_aux (Nat.S n) (Cons N 5) --> decimal_aux n (Cons N 6).
[n,N] decimal_aux (Nat.S n) (Cons N 6) --> decimal_aux n (Cons N 7).
[n,N] decimal_aux (Nat.S n) (Cons N 7) --> decimal_aux n (Cons N 8).
[n,N] decimal_aux (Nat.S n) (Cons N 8) --> decimal_aux n (Cons N 9).
[n,N] decimal_aux (Nat.S n) (Cons N 9) --> decimal_aux n (Cons (decimal_aux (Nat.S Nat.0) N) 0).
def binary : tuto.Nat -> Number.
def binary_aux : tuto.Nat -> Number -> Number.
def binary : Nat.t -> Number.
def binary_aux : Nat.t -> Number -> Number.
[n] binary n --> binary_aux n Zero.
[N] binary_aux tuto.0 N --> N.
[n] binary_aux (tuto.S n) Zero --> binary_aux n (Cons Zero 1).
[n,N] binary_aux (tuto.S n) (Cons N 0) --> binary_aux n (Cons N 1).
[n,N] binary_aux (tuto.S n) (Cons N 1) --> binary_aux n (Cons (decimal_aux (tuto.S tuto.0) N) 0).
[N] binary_aux Nat.0 N --> N.
[n] binary_aux (Nat.S n) Zero --> binary_aux n (Cons Zero 1).
[n,N] binary_aux (Nat.S n) (Cons N 0) --> binary_aux n (Cons N 1).
[n,N] binary_aux (Nat.S n) (Cons N 1) --> binary_aux n (Cons (decimal_aux (Nat.S Nat.0) N) 0).
def hexadecimal : tuto.Nat -> Number.
def hexadecimal_aux : tuto.Nat -> Number -> Number.
def hexadecimal : Nat.t -> Number.
def hexadecimal_aux : Nat.t -> Number -> Number.
[n] hexadecimal n --> hexadecimal_aux n Zero.
[N] hexadecimal_aux tuto.0 N --> N.
[n] hexadecimal_aux (tuto.S n) Zero --> hexadecimal_aux n (Cons Zero 1).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 0) --> hexadecimal_aux n (Cons N 1).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 1) --> hexadecimal_aux n (Cons N 2).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 2) --> hexadecimal_aux n (Cons N 3).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 3) --> hexadecimal_aux n (Cons N 4).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 4) --> hexadecimal_aux n (Cons N 5).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 5) --> hexadecimal_aux n (Cons N 6).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 6) --> hexadecimal_aux n (Cons N 7).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 7) --> hexadecimal_aux n (Cons N 8).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 8) --> hexadecimal_aux n (Cons N 9).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 9) --> hexadecimal_aux n (Cons N A).
[n,N] hexadecimal_aux (tuto.S n) (Cons N A) --> hexadecimal_aux n (Cons N B).
[n,N] hexadecimal_aux (tuto.S n) (Cons N B) --> hexadecimal_aux n (Cons N C).
[n,N] hexadecimal_aux (tuto.S n) (Cons N C) --> hexadecimal_aux n (Cons N D).
[n,N] hexadecimal_aux (tuto.S n) (Cons N D) --> hexadecimal_aux n (Cons N E).
[n,N] hexadecimal_aux (tuto.S n) (Cons N E) --> hexadecimal_aux n (Cons N F).
[n,N] hexadecimal_aux (tuto.S n) (Cons N F) --> hexadecimal_aux n (Cons (hexadecimal_aux (tuto.S tuto.0) N) 0).
[N] hexadecimal_aux Nat.0 N --> N.
[n] hexadecimal_aux (Nat.S n) Zero --> hexadecimal_aux n (Cons Zero 1).
[n,N] hexadecimal_aux (Nat.S n) (Cons N 0) --> hexadecimal_aux n (Cons N 1).
[n,N] hexadecimal_aux (Nat.S n) (Cons N 1) --> hexadecimal_aux n (Cons N 2).
[n,N] hexadecimal_aux (Nat.S n) (Cons N 2) --> hexadecimal_aux n (Cons N 3).
[n,N] hexadecimal_aux (Nat.S n) (Cons N 3) --> hexadecimal_aux n (Cons N 4).
[n,N] hexadecimal_aux (Nat.S n) (Cons N 4) --> hexadecimal_aux n (Cons N 5).
[n,N] hexadecimal_aux (Nat.S n) (Cons N 5) --> hexadecimal_aux n (Cons N 6).
[n,N] hexadecimal_aux (Nat.S n) (Cons N 6) --> hexadecimal_aux n (Cons N 7).
[n,N] hexadecimal_aux (Nat.S n) (Cons N 7) --> hexadecimal_aux n (Cons N 8).
[n,N] hexadecimal_aux (Nat.S n) (Cons N 8) --> hexadecimal_aux n (Cons N 9).
[n,N] hexadecimal_aux (Nat.S n) (Cons N 9) --> hexadecimal_aux n (Cons N A).
[n,N] hexadecimal_aux (Nat.S n) (Cons N A) --> hexadecimal_aux n (Cons N B).
[n,N] hexadecimal_aux (Nat.S n) (Cons N B) --> hexadecimal_aux n (Cons N C).
[n,N] hexadecimal_aux (Nat.S n) (Cons N C) --> hexadecimal_aux n (Cons N D).
[n,N] hexadecimal_aux (Nat.S n) (Cons N D) --> hexadecimal_aux n (Cons N E).
[n,N] hexadecimal_aux (Nat.S n) (Cons N E) --> hexadecimal_aux n (Cons N F).
[n,N] hexadecimal_aux (Nat.S n) (Cons N F) --> hexadecimal_aux n (Cons (hexadecimal_aux (Nat.S Nat.0) N) 0).
......@@ -4,4 +4,4 @@ def lamt : Type.
def delta : lamt := (x => x x).
def omega : lamt := delta delta.
#EVAL[HNF] (x: lamt => (y: lamt => y)) omega.
#EVAL[WHNF] (x: lamt => (y: lamt => y)) omega.
......@@ -30,11 +30,6 @@ def operation4 : Nat -> Nat -> Nat.
#EVAL[SNF] operation3 (operation3 (S 0) (S 0)) (S 0).
#EVAL[SNF] operation4 (operation4 (S 0) (S 0)) (S 0).
#EVAL[HNF] operation (S 0) (S 0).
#EVAL[HNF] operation2 (S 0) (S 0).
#EVAL[HNF] operation3 (operation3 (S 0) (S 0)) (S 0).
#EVAL[HNF] operation4 (operation4 (S 0) (S 0)) (S 0).
#EVAL[WHNF] operation (S 0) (S 0).
#EVAL[WHNF] operation2 (S 0) (S 0).
#EVAL[WHNF] operation3 (operation3 (S 0) (S 0)) (S 0).
......
A:Type.
a:A.
def b:A.
def f:A->A.
def g:(A->A)->A.
[] b --> a.
[] f b --> a.
[] g (x => b) --> a.
#EVAL[WHNF] f b.
#EVAL[WHNF] g (x => b).
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