Commit 5515208f authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Remove polymorphic if

parent 100ffcad
......@@ -27,22 +27,6 @@ match :
Hf : eT (P false) ]
match P Ht Hf false --> Hf.
(; Operations ;)
(; polymorphic if .. then .. else .. ;)
ite :
A : uT ->
Bool ->
eT A ->
eT A ->
eT A.
[ A : uT,
x : eT A,
y : eT A,
b : Bool ]
ite A b x y
-->
match (b : Bool => A) x y b.
(; boolean if .. then .. else .. ;)
iteb : Bool -> Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] iteb true x y --> x
......
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