# [Agda] `postulate' in `let'

Serge D. Mechveliani mechvel at botik.ru
Thu Aug 23 11:31:32 CEST 2012

```Can you, please, explain the difference of `where' and `let' constructs
with respect to `postulate' ?
Consider the following small program using
(in which I replace the math symbols with  Nat  and  `subtract'):

------------------------------------------
lessNat? : Nat -> Nat -> Bool
lessNat? 0       0       = false
lessNat? 0       (suc _) = true
lessNat? (suc _) 0       = false
lessNat? (suc n) (suc m) = lessNat? n m

LessNat? : Nat -> Nat -> Set
LessNat? n m = T (lessNat? n m)

f : (n : Nat) -> LessNat? 7 n -> Nat
f n _ = subtract n 8                  -- subtract = \.-  -- math symbol

g : Nat -> Nat
g n = f m p  where
m = (n + 3) * (n + 3)
postulate p : LessNat? 7 m

-- I am testing `postulate' because I imagine for  m  some expression of
-- which value I am sure that it is greater than 7, and which formal
-- inequality proof is difficult to provide.

g2 : Nat -> Nat                       -- a variant of  g
g2 n = let m = (n + 3) * (n + 3)
postulate p : LessNat? 7 m
in  f m p

h : Nat -> Nat
h n = let L7 : Set           -- just some test example with `let'
L7 = LessNat? 7 n
h' : Nat -> Nat
h' n = n + 2
in  h' (n * n)
-------------------------------------------

Now,  g  and  h  are compiled,
and  g2  is not:
"Not a valid let-declaration when scope checking".

What is the meaning of this difference?
Thanks,

------
Sergei
```