Skip to content

C
cpdt
Commit 1c4b6709 authored by Adam Chlipala's avatar Adam Chlipala
Browse files
Options

thide parsing-motivating definitions at start of Predicates

parent 02beda15
Show whitespace changes
Inline Side-by-side
Showing with 2 additions and 0 deletions
src/Predicates.v
View file @ 1c4b6709
...@@ -16,6 +16,7 @@ Set Implicit Arguments. ...@@ -16,6 +16,7 @@ Set Implicit Arguments.
(* Extra definitions to get coqdoc to choose the right fonts. *) (* Extra definitions to get coqdoc to choose the right fonts. *)
(* begin thide *)
Inductive unit := tt. Inductive unit := tt.
Inductive Empty_set := . Inductive Empty_set := .
Inductive bool := true | false. Inductive bool := true | false.
...@@ -26,6 +27,7 @@ Inductive or := or_introl | or_intror. ...@@ -26,6 +27,7 @@ Inductive or := or_introl | or_intror.
Inductive ex := ex_intro. Inductive ex := ex_intro.
Inductive eq := refl_equal. Inductive eq := refl_equal.
Reset unit. Reset unit.
(* end thide *)
(* end hide *) (* end hide *)
(** %\chapter{Inductive Predicates}% *) (** %\chapter{Inductive Predicates}% *)
......
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