Nicolas Magaud - Coq - Computing power(x,n) efficiently

Various Styles of Programming in Coq: computing power(x,n) efficiently


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (84 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (67 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (11 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (6 entries)

Global Index

F

F [definition, in power_ind]
F [definition, in power_iter]
F [definition, in power_cps]
F [definition, in power]
F [definition, in power2]


L

lemmas [library]
local_proof_irr [lemma, in power_cps]
local_proof_irr [lemma, in power2]
local_proof_irr [lemma, in power_iter]
local_proof_irr [lemma, in power]
lt_minus_1 [lemma, in lemmas]


M

mult_diff [lemma, in lemmas]


N

not_zero_implies_pos_or_neg [lemma, in lemmas]
not_zero_implies_square_pos [lemma, in lemmas]


O

odd_even_minus [lemma, in lemmas]


P

power [definition, in power]
power [definition, in power_cps]
power [definition, in power2]
power [definition, in power_iter]
power [library]
power2 [library]
power_cps [library]
power_ind [definition, in power_ind]
power_ind [library]
power_iter [library]
power_neg_even_pos [lemma, in power_iter]
power_neg_even_pos [lemma, in power_cps]
power_neg_even_pos [lemma, in power2]
power_neg_even_pos [lemma, in power]
power_neg_odd_neg [lemma, in power]
power_neg_odd_neg [lemma, in power_cps]
power_neg_odd_neg [lemma, in power_iter]
power_neg_odd_neg [lemma, in power2]
power_neg_odd_neg_aux1 [lemma, in power_iter]
power_neg_odd_neg_aux1 [lemma, in power_cps]
power_neg_odd_neg_aux2 [lemma, in power_cps]
power_neg_odd_neg_aux2 [lemma, in power_iter]
power_neg_odd_neg_aux3 [lemma, in power_iter]
power_neg_odd_neg_aux3 [lemma, in power_cps]
power_not_zero [lemma, in power_iter]
power_not_zero [lemma, in power]
power_not_zero [lemma, in power_cps]
power_not_zero [lemma, in power2]
power_not_zero_aux [lemma, in power_cps]
power_not_zero_aux [lemma, in power_iter]
power_pos_pos [lemma, in power]
power_pos_pos [lemma, in power2]
power_pos_pos [lemma, in power_iter]
power_pos_pos [lemma, in power_cps]
power_pos_pos_aux [lemma, in power_iter]
power_pos_pos_aux [lemma, in power_cps]


R

real_red1 [lemma, in power2]
real_red1 [lemma, in power_cps]
real_red1 [lemma, in power_iter]
real_red1 [lemma, in power]
real_red2 [lemma, in power_cps]
real_red2 [lemma, in power2]
real_red2 [lemma, in power_iter]
real_red2 [lemma, in power]
real_red3 [lemma, in power2]
real_red3 [lemma, in power_cps]
real_red3 [lemma, in power]
real_red3 [lemma, in power_iter]
red [lemma, in power]
red [lemma, in power_iter]
red [lemma, in power_cps]
red [lemma, in power2]
reduction_1 [lemma, in power]
reduction_1 [lemma, in power_iter]
reduction_1 [lemma, in power_cps]
reduction_1 [lemma, in power2]
reduction_2 [lemma, in power]
reduction_2 [lemma, in power_cps]
reduction_2 [lemma, in power2]
reduction_2 [lemma, in power_iter]
reduction_5 [lemma, in power_iter]
reduction_5 [lemma, in power_cps]
reduction_5 [lemma, in power]
reduction_5 [lemma, in power2]


S

signe1 [lemma, in lemmas]
signe2 [lemma, in lemmas]
signe3 [lemma, in lemmas]
signe4 [lemma, in lemmas]
sqr [definition, in lemmas]



Lemma Index

L

local_proof_irr [in power_cps]
local_proof_irr [in power2]
local_proof_irr [in power_iter]
local_proof_irr [in power]
lt_minus_1 [in lemmas]


M

mult_diff [in lemmas]


N

not_zero_implies_pos_or_neg [in lemmas]
not_zero_implies_square_pos [in lemmas]


O

odd_even_minus [in lemmas]


P

power_neg_even_pos [in power_iter]
power_neg_even_pos [in power_cps]
power_neg_even_pos [in power2]
power_neg_even_pos [in power]
power_neg_odd_neg [in power]
power_neg_odd_neg [in power_cps]
power_neg_odd_neg [in power_iter]
power_neg_odd_neg [in power2]
power_neg_odd_neg_aux1 [in power_iter]
power_neg_odd_neg_aux1 [in power_cps]
power_neg_odd_neg_aux2 [in power_cps]
power_neg_odd_neg_aux2 [in power_iter]
power_neg_odd_neg_aux3 [in power_iter]
power_neg_odd_neg_aux3 [in power_cps]
power_not_zero [in power_iter]
power_not_zero [in power]
power_not_zero [in power_cps]
power_not_zero [in power2]
power_not_zero_aux [in power_cps]
power_not_zero_aux [in power_iter]
power_pos_pos [in power]
power_pos_pos [in power2]
power_pos_pos [in power_iter]
power_pos_pos [in power_cps]
power_pos_pos_aux [in power_iter]
power_pos_pos_aux [in power_cps]


R

real_red1 [in power2]
real_red1 [in power_cps]
real_red1 [in power_iter]
real_red1 [in power]
real_red2 [in power_cps]
real_red2 [in power2]
real_red2 [in power_iter]
real_red2 [in power]
real_red3 [in power2]
real_red3 [in power_cps]
real_red3 [in power]
real_red3 [in power_iter]
red [in power]
red [in power_iter]
red [in power_cps]
red [in power2]
reduction_1 [in power]
reduction_1 [in power_iter]
reduction_1 [in power_cps]
reduction_1 [in power2]
reduction_2 [in power]
reduction_2 [in power_cps]
reduction_2 [in power2]
reduction_2 [in power_iter]
reduction_5 [in power_iter]
reduction_5 [in power_cps]
reduction_5 [in power]
reduction_5 [in power2]


S

signe1 [in lemmas]
signe2 [in lemmas]
signe3 [in lemmas]
signe4 [in lemmas]



Definition Index

F

F [in power_ind]
F [in power_iter]
F [in power_cps]
F [in power]
F [in power2]


P

power [in power]
power [in power_cps]
power [in power2]
power [in power_iter]
power_ind [in power_ind]


S

sqr [in lemmas]



Library Index

L

lemmas


P

power
power2
power_cps
power_ind
power_iter



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (84 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (67 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (11 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (6 entries)

This page has been generated by coqdoc