Zulip Chat Archive

Stream: new members

Topic: cannot reduce application in pattern match


view this post on Zulip Shaun Steenkamp (Nov 14 2018 at 11:58):

I'm trying to fill in the sorry in the code below with h x. I expect this to work but it says that

26:23: equation type mismatch, term
  h x
has type
  f x = g x
but is expected to have type
  k x st.s = k x st.t

even though I define k x st.s =def= f x and k x st.t =def= g x

code:

universe 
universe ℓ'

inductive st : Type
|  s : st
|  t : st

inductive R : st  st  Type
| r : R st.s st.t

def fex
  {A : Type }
  {B : A  Type ℓ'}
  {f g : Π (x : A) , B x}
  (h : Π (x : A) , f x = g x)
  : -------------------------
  (A  A)
:=
  have k : Π (x : A) (_ : st) , B x, from
    λ x h , match h with
      | st.s := f x
      | st.t := g x
    end,
  have l : Π (x : A)(b b' : st)(_ : R b b') , k x b = k x b', from
    λ x b b' r' , match b, b', r' with
      st.s, st.t, R.r := sorry -- h x
    end,
  show A  A, from λ x , x

Can someone tell me why it's not reducing?

view this post on Zulip Mario Carneiro (Nov 14 2018 at 12:15):

use let instead of have

view this post on Zulip Shaun Steenkamp (Nov 14 2018 at 12:19):

okay, now I get a message saying I need to use set_option eqn_compiler.zeta true

view this post on Zulip Shaun Steenkamp (Nov 14 2018 at 12:20):

and then it works fine


Last updated: May 14 2021 at 23:14 UTC