Skip to content

Instantly share code, notes, and snippets.

@Lysxia

Lysxia/STO.v

Created December 14, 2023 10:43
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Lysxia/4702f10f92d51d79dfdb65dbc40b6d7b to your computer and use it in GitHub Desktop.
Save Lysxia/4702f10f92d51d79dfdb65dbc40b6d7b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
STO.v
(* A trick to print the simplified type of something *)
Definition type_of {A : Type} (a : A) : Type := A.
Arguments type_of _ /.
Notation simpl_type_of a := ltac:(let A := eval simpl in (type_of a) in exact A).
(* Example *)
Parameter p : forall x, 3 + x = x.
Check (simpl_type_of p).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment