Skip to content

Instantly share code, notes, and snippets.

@wires

wires/*scratch*

Created November 11, 2011 00:07
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 wires/1356700 to your computer and use it in GitHub Desktop.
Save wires/1356700 to your computer and use it in GitHub Desktop.
Download ZIP
Problems defining a coercion between product types
Raw
*scratch*
Infix "×" := prod (at level 60).
Coercion bool_in_nat := fun b:bool => if b then 0 else 1.
Definition a : nat := false.
Definition foo (p:bool × bool) : bool × nat :=
(fst p, snd p:nat).
Coercion fooc := foo.
(* Error: fooc does not respect the uniform inheritance condition.
Q1: Can you define such a coercion from A × B → A × C ?
Q2: What is the uniform inheritance condition?
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment