Simple type mismatch

Stream: general

[Spencer Killen]

Hello

I am learning LEAN and have run into an issue with the following code:

inductive Literal (term: Term)
| pos (term: Term)  : Literal
| neg (term: Term) : Literal
#check set Literal

The type checker complains about the #check line and I'm not sure why

set : Type u → Type u
type mismatch at application
  set Literal
term
  Literal
has type
  Π (Term : Prop), Term → Type : Type 1
but is expected to have type
  Type ? : Type (?+1)Lean

If someone could help explain what the issue is or point me in the right direction I'd be greatly appreciative

[Yury G. Kudryashov]

You can use set (Literal nat)

[Yury G. Kudryashov]

Literal is a function that takes a type Term, and returns a new type.

[Yury G. Kudryashov]

You need to apply it to some type to get a Type

[Yury G. Kudryashov]

UPD: how do you define Term?

[Yury G. Kudryashov]

It seems that Literal takes an argument of type Term, not Type

[Spencer Killen]

Thanks,
Term is

variable Term : Prop

I think I'm going about this the wrong way...

[Yury G. Kudryashov]

What are you trying to achieve?

[Spencer Killen]

I'd like a set of elements that are each either of the variants of Literal

[Reid Barton]

I think your definition of Literal does not mean what you think.

[Reid Barton]

And probably Term as well.

[Spencer Killen]

probably not...

[Yury G. Kudryashov]

So please explain what do you want to achieve with your definitions of Term and Literal

[Reid Barton]

I would guess what you want is

inductive Literal (Term : Type)
| pos (term: Term)  : Literal
| neg (term: Term) : Literal

[Mario Carneiro]

Or possibly

inductive Literal
| pos (term: Term)  : Literal
| neg (term: Term) : Literal

where Term has previously been defined

[Reid Barton]

Yes, I started with that, then changed my mind for some reason, but probably you are right

[Spencer Killen]

I want to define a type, Interpretation that is a set of literals where a literal is either true or false and has an associated Term
I realize I could probably accomplish much of this with the standard lib but it's a learning process :sweat_smile:

[Mario Carneiro]

What is a Term though

[Spencer Killen]

I'm not really sure, in my code so far I have it as a Prop

[Mario Carneiro]

It should probably be a Type, not a Prop

[Yury G. Kudryashov]

What do you want to do with these types?

[Spencer Killen]

I'm writing stuff for stable model semantics. Just seeing if I can do some basic theorems

[Mario Carneiro]

so what's the thing you want to define/prove?

[Spencer Killen]

I'd like to prove that an interpretation is a model for a logic program
I thought I'd define all the constructs before hand but maybe that isn't the best place to start

[Spencer Killen]

I'm going to try getting rid of the parameter on Literal like you suggested and see if that gets me where I want

[Kenny Lau]

how about write down the mathematical definitions first

[Reid Barton]

This logic-type stuff can actually be pretty tricky to formalize even when in a sense nothing much is happening. I mean everyone "knows" what a real number is--if you don't really know what one is then you still know that it corresponds to the type real; but it's not so easy to say what a variable is. It doesn't help that sources usually don't explain very clearly what they mean, either.