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

fix: ToExpr instance for Fin

Browse source
This commit is contained in:
Leonardo de Moura 2024-02-23 21:14:17 -08:00 • committed by Leonardo de Moura
parent 6d569aa7b5
commit 66be8b9d4c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/ToExpr.lean
View file

@ -48,7 +48,7 @@ instance : ToExpr (Fin n) where
toExpr a :=
let r := mkRawNatLit a.val
mkApp3 (.const ``OfNat.ofNat [0]) (.app (mkConst ``Fin) (toExpr n)) r
(mkApp2 (.const ``Fin.instOfNat []) (mkRawNatLit (n-1)) r)
(mkApp2 (.const ``Fin.instOfNat []) (mkNatLit (n-1)) r)
instance : ToExpr (BitVec n) where
toTypeExpr := .app (mkConst ``BitVec) (toExpr n)