Commit bced5a29 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Merge branch 'master' of https://git.lsv.fr/genestier/PleinDeDk

parents bce92954 7d8ed428
Nat : Type.
A : Type.
List : Type.
Bool : Type.
0 : Nat.
S : Nat -> Nat.
True : Bool.
False : Bool.
Nil : List.
Cons : (n: Nat) -> A -> List -> List.
def taut : A -> Bool.
[] taut _ --> True.
(;
def ifthensucc : Bool -> Nat -> Nat.
[n] ifthensucc True n --> S n.
[n] ifthensucc False n --> n.
(; ;)
def compute_length : (A -> Bool) -> (n: Nat) -> List -> Nat.
def aux_length : Bool -> (A -> Bool) -> (n: Nat) -> List -> Nat.
[] compute_length _ _ Nil --> 0.
[f,n,x,l] compute_length f _ (Cons n x l) --> aux_length (f x) f n l.
[n,l] compute_length taut n l --> n.
[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 -> List.
def bis : b: Bool -> f: (A -> Bool) -> x: A -> (n: Nat) -> l: List -> List.
[] filter _ _ Nil --> Nil.
[f,n,x,l] filter f _ (Cons n x l) --> bis (f x) f x n l.
[l] filter taut _ l --> 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