max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: reflective inductive predicate

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-25 20:35:13 -07:00
parent a04f3a5d9f
commit af391fe812
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/run/reflectiveIndPred.lean Normal file
View file

@ -0,0 +1,12 @@
inductive Expr where
| val : Nat → Expr
| add : Expr → Expr → Expr
| fn : (Nat → Expr) → Expr
inductive Pos : Expr → Prop
| base : (n : Nat) → Pos (Expr.val n.succ)
| add : Pos e₁ → Pos e₂ → Pos (Expr.add e₁ e₂)
| fn : ((n : Nat) → Pos (f n)) → Pos (Expr.fn f)
#print PosProofBelow
#print Pos.brecOn