Skip to content
GitLab
Commit a3513e04 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

small alignment

parent e6f3cab8
Hide whitespace changes
Inline Side-by-side
paper/5_highlevel.tex
View file @ a3513e04
......@@ -391,7 +391,6 @@ Inductive type := Zmodp x of betweenb 0 p x.
Lemma Z_mod_betweenb (x y : Z) :
y > 0 -> betweenb 0 y (x mod y).
Definition pi (x : Z) : type :=
Zmodp (Z_mod_betweenb x Hp_gt0).
Coercion repr (x : type) : Z :=
......
Supports Markdown
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