Why aren't these equivalent? (helper for creating subsets)

Stream: general

[Marvin]

I'm trying to create a helper function to create subsets for dsl purposes.

import Mathlib.Data.Set.Basic

-- approach 1
def a := {x : Nat | x > 0}

-- approach 2
axiom S (p : X → Prop) : {x : X | p x}

def b := S (· > 0) -- I want this notation to work
-- error `S` not supported by code generator;
-- consider marking definition as `noncomputable`

I assumed that the two approaches would be equivalent; the type inference would see that the lambda (· > 0) is a Nat -> Prop, in which case it should then conclude that {x : X | p x} is {x : Nat | p x}, which is identical to approach 1. Yet it fails.

I want it to be true that a = b

[Marvin]

ah, it looks like I just need to use abbrev and not axiom. Curious why that is?

[Yury G. Kudryashov]

It's because abbrev adds a reducible definition, and axiom adds... an axiom.

[Eric Wieser]

You're also confusing : with := there