senvas/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

coq: remove type_unit & type_num

Browse source
This commit is contained in:
Michael Sippel 2024-08-21 16:10:15 +02:00
parent 42ae93f2d7
commit 0caf3ff514
Signed by: senvas
GPG key ID: 060F22F65102F95C
2 changed files with 2 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
coq/equiv.v
View file

@ -224,9 +224,7 @@ Qed.
(** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
Inductive type_is_flat : type_term -> Prop :=
| FlatUnit : (type_is_flat type_unit)
| FlatVar : forall x, (type_is_flat (type_var x))
| FlatNum : forall x, (type_is_flat (type_num x))
| FlatId : forall x, (type_is_flat (type_id x))
| FlatApp : forall x y,
(type_is_flat x) ->
@ -295,22 +293,11 @@ Proof.
intros.
destruct t.
exists type_unit.
split. apply TEq_Refl.
apply LNF.
admit.
exists (type_id s).
split. apply TEq_Refl.
apply LNF.
admit.
admit.
exists (type_num n).
split. apply TEq_Refl.
apply LNF.
admit.
admit.
exists (type_univ s t).
@ -342,11 +329,11 @@ Admitted.
*)
Example example_flat_type :
(type_is_flat (type_spec (type_id "PosInt") (type_num 10))).
(type_is_flat (type_spec (type_id "PosInt") (type_id "10"))).
Proof.
apply FlatApp.
apply FlatId.
apply FlatNum.
apply FlatId.
Qed.
Example example_lnf_type :

2
coq/terms.v
View file

@ -8,10 +8,8 @@ Module Terms.
(* types *)
Inductive type_term : Type :=
| type_unit : type_term
| type_id : string -> type_term
| type_var : string -> type_term
| type_num : nat -> type_term
| type_fun : type_term -> type_term -> type_term
| type_univ : string -> type_term -> type_term
| type_spec : type_term -> type_term -> type_term