Commit e0805468 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Small cleaning

parent b441c56a
Nat : Type.
0 : Nat.
S : Nat -> Nat.
def plus : Nat -> Nat -> Nat.
[y] plus 0 y --> y.
[x,y] plus (S x) y --> S (plus x y).
def mult : Nat -> Nat -> Nat.
[] mult 0 _ --> 0.
[x,y] mult (S x) y --> plus (mult x y) y.
def g : Nat -> Nat.
def f : Nat -> Nat -> Nat.
[x] f x x --> g x.
[x,y] g (plus (S x) (S y)) --> f (plus (S x) (S y)) (mult (S x) y).
#EVAL g (plus (S (S (S 0))) (S (S (S 0)))).
\ No newline at end of file
Nat : Type.
A : Type.
List : Nat -> Type.
Bool : Type.
0 : Nat.
S : Nat -> Nat.
True : Bool.
False : Bool.
Nil : List 0.
Cons : (n: Nat) -> A -> List n -> List (S n).
def ifthensucc : Bool -> Nat -> Nat.
[n] ifthensucc True n --> S n.
[n] ifthensucc False n --> n.
def compute_length : (A -> Bool) -> (n: Nat) -> List n -> Nat.
def aux_length : Bool -> (A -> Bool) -> (n: Nat) -> List n -> Nat.
[f,n,x,l] compute_length f _ (Cons n x l) --> aux_length (f x) f n l.
[f,n,l] aux_length True f n l --> S (compute_length f n l).
[f,n,l] aux_length False f n l --> compute_length f n l.
def filter : f: (A -> Bool) -> (n: Nat) -> l: List n -> List (compute_length f n l).
def bis : b: Bool -> f: (A -> Bool) -> x: A -> (n: Nat) -> l: List n -> List (aux_length b f n l).
[f,n,x,l] filter f _ (Cons n x l) --> bis (f x) f x n l.
[f,n,x,l] bis True f x n l --> Cons (compute_length f n l) x (filter f n l).
[f,x,n,l] bis False f x n l --> filter f n l.
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