puzzle: subst syntax

Stream: general

[Joachim Breitner]

Another small puzzle:
Which of these definitions are accepted, and those without an explicit return type, what is their inferred return type:

def foo := 3
def bar := 4

def ex1  (heq : foo = bar) (P : Nat → Prop) (h : P foo)         := heq ▸ h
def ex2  (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P 4   := heq ▸ h
def ex3  (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P bar := heq ▸ h
def ex4  (heq : foo = bar) (P : Nat → Prop) (h : P 3)           := heq ▸ h
def ex5  (heq : foo = bar) (P : Nat → Prop) (h : P 3)   : P 4   := heq ▸ h
def ex6  (heq : foo = bar) (P : Nat → Prop) (h : P 3)   : P bar := heq ▸ h

def ex7  (heq : bar = foo) (P : Nat → Prop) (h : P foo)         := heq ▸ h
def ex8  (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P 4   := heq ▸ h
def ex9  (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P bar := heq ▸ h
def ex10 (heq : bar = foo) (P : Nat → Prop) (h : P 3)           := heq ▸ h
def ex11 (heq : bar = foo) (P : Nat → Prop) (h : P 3)   : P 4   := heq ▸ h
def ex12 (heq : bar = foo) (P : Nat → Prop) (h : P 3)   : P bar := heq ▸ h

[Floris van Doorn]

I think that the second occurrences of foo and bar are not accepted :-)

[Joachim Breitner]

Vote passed