heap instants

Stream: lean4

[elisheva morgenstern]

Hello, I'm new here, I wanted to ask:
I have an inductive heap and I can't get an instant out of it in a way that I can look at the input and output of elements.
It has a leaf and a node with right key value and left

[Kim Morrison]

Can you show us a #mwe?

[elisheva morgenstern]

I have this code:
inductive Heap (h : Type v) where
| leaf
| node (left : Heap h) (key : Nat) (value : h) (right : Heap h)
deriving Repr

def insert {h : Type u} (t : Heap h) (k : Nat) (v : h) : Heap h :=
.........

here I want to check the insert and tried a lot of things

[Kevin Buzzard]

You could edit your previous post once you've learnt about #backticks and it will be nicer to read

[Thomas Murrills]

Hello, welcome! What do you mean by "check the insert" here and what do you mean by "instant"? (Also do please edit your messages to use #backticks as mentioned!)

[Thomas Murrills]

In case what you want involves getting the arguments of Heap.node, is syntax like

match t with
| .leaf => sorry
| .node l k v r => sorry -- <do something with `l`, `k`, `v`, and `r`>

familiar to you?

[elisheva morgenstern]

Hey thanks you!
Either it gave me an error or I didn't fully understand how to connect it to the code.
I also tried to print with IO Unit but I failed.
I am trying to send again in the format:

'''
import Lean

inductive Heap (h : Type v) where
| leaf
| node (left : Heap h) (key : Nat) (value : h) (right : Heap h)
deriving Repr

-- #check Nat

def insert {h : Type u} (t : Heap h) (k : Nat) (v : h) : Heap h :=
let rec insertAux : Heap h → Heap h :=
λ tree =>
match tree with
| Heap.leaf => Heap.node Heap.leaf k v Heap.leaf
| Heap.node l key value r =>
if k < key then
Heap.node (insertAux l) key value r
else
Heap.node l key value (insertAux r)
match t with
| Heap.leaf => Heap.node Heap.leaf k v Heap.leaf
| _ => insertAux t
'''

it is ok?

[Patrick Massot]

Zulip tip: you are using the wrong kind of quotation marks: you need `

[Kim Morrison]

(You are much more likely to get answers if you follow the requests above about #backticks. e.g. it lets others open your code in the online editor, and be more confident that the code will run locally if they want to.)